Anne is rough. Fiona is nice. Fiona is not rough. Gary is blue. Gary is not white. Harry is round. Harry is white. All smart, white people are blue. Rough, round people are blue. If someone is nice and rough then they are blue. If someone is big then they are round. If Anne is nice and Anne is round then Anne is smart. All rough people are nice. If someone is nice then they are big. All smart, big people are white.
Anne is rough.
("Anne" "is" "rough" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is not rough.
("Fiona" "is" "rough" "-")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is not white.
("Gary" "is" "white" "-")
Harry is round.
("Harry" "is" "round" "+")
Harry is white.
("Harry" "is" "white" "+")
All smart, white people are blue.
((("someone" "is" "smart" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "blue" "+"))
Rough, round people are blue.
((("someone" "is" "rough" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "blue" "+"))
If someone is nice and rough then they are blue.
((("someone" "is" "nice" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "blue" "+"))
If someone is big then they are round.
((("someone" "is" "big" "+")) -> ("someone" "is" "round" "+"))
If Anne is nice and Anne is round then Anne is smart.
((("Anne" "is" "nice" "+") ("Anne" "is" "round" "+")) -> ("Anne" "is" "smart" "+"))
All rough people are nice.
((("someone" "is" "rough" "+")) -> ("someone" "is" "nice" "+"))
If someone is nice then they are big.
((("someone" "is" "nice" "+")) -> ("someone" "is" "big" "+"))
All smart, big people are white.
((("someone" "is" "smart" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "white" "+"))
Fiona is not rough.
True
1
proof
[(triple3)]
("Fiona" "is" "rough" "-")
triple3
Harry is not round.
False
1
inv-proof
[(triple6)]
("Harry" "is" "round" "-")
triple6
Anne is nice.
True
2
proof
[(((triple1) -> rule6))]
("Anne" "is" "nice" "+")
((triple1) -> (rule6 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Fiona is not big.
False
2
inv-proof
[(((triple2) -> rule7))]
("Fiona" "is" "big" "-")
((triple2) -> (rule7 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Anne is big.
True
3
proof
[(((((triple1) -> rule6)) -> rule7))]
("Anne" "is" "big" "+")
((((triple1) -> (rule6 % int2))) -> (rule7 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Fiona is not round.
False
3
inv-proof
[(((((triple2) -> rule7)) -> rule4))]
("Fiona" "is" "round" "-")
((((triple2) -> (rule7 % int2))) -> (rule4 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Anne is round.
True
4
proof
[(((((((triple1) -> rule6)) -> rule7)) -> rule4))]
("Anne" "is" "round" "+")
((((((triple1) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is not round.
False
4
inv-proof
[(((((((triple1) -> rule6)) -> rule7)) -> rule4))]
("Anne" "is" "round" "-")
((((((triple1) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is smart.
True
7
proof
[(((((triple1) -> rule6) ((((((triple1) -> rule6)) -> rule7)) -> rule4)) -> rule5))]
("Anne" "is" "smart" "+")
((((triple1) -> (rule6 % int4)) ((((((triple1) -> (rule6 % int4))) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Anne is nice.
("Anne" "is" "nice" "+")
int4
Anne is not smart.
False
7
inv-proof
[(((((triple1) -> rule6) ((((((triple1) -> rule6)) -> rule7)) -> rule4)) -> rule5))]
("Anne" "is" "smart" "-")
((((triple1) -> (rule6 % int4)) ((((((triple1) -> (rule6 % int4))) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Anne is nice.
("Anne" "is" "nice" "+")
int4
Anne is white.
True
11
proof
[(((((((triple1) -> rule6) ((((((triple1) -> rule6)) -> rule7)) -> rule4)) -> rule5) ((((triple1) -> rule6)) -> rule7)) -> rule8))]
("Anne" "is" "white" "+")
((((((triple1) -> (rule6 % int5)) ((((((triple1) -> (rule6 % int5))) -> (rule7 % int4))) -> (rule4 % int3))) -> (rule5 % int2)) ((((triple1) -> (rule6 % int5))) -> (rule7 % int4))) -> (rule8 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Anne is big.
("Anne" "is" "big" "+")
int4
Anne is nice.
("Anne" "is" "nice" "+")
int5
Anne is not white.
False
11
inv-proof
[(((((((triple1) -> rule6) ((((((triple1) -> rule6)) -> rule7)) -> rule4)) -> rule5) ((((triple1) -> rule6)) -> rule7)) -> rule8))]
("Anne" "is" "white" "-")
((((((triple1) -> (rule6 % int5)) ((((((triple1) -> (rule6 % int5))) -> (rule7 % int4))) -> (rule4 % int3))) -> (rule5 % int2)) ((((triple1) -> (rule6 % int5))) -> (rule7 % int4))) -> (rule8 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Anne is big.
("Anne" "is" "big" "+")
int4
Anne is nice.
("Anne" "is" "nice" "+")
int5
Harry is not blue.
Unknown
inv-rconc
[@1: Harry is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "blue" "-")
Gary is big.
Unknown
rconc
[@2: Gary is big.[CWA. Example of deepest failure = (rule7 <- rule6 <- FAIL)]]
("Gary" "is" "big" "+")
Gary is not round.
Unknown
inv-rconc
[@3: Gary is round.[CWA. Example of deepest failure = (rule4 <- rule7 <- rule6 <- FAIL)]]
("Gary" "is" "round" "-")
Fiona is blue.
Unknown
rconc
[@1: Fiona is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "blue" "+")
Harry is not nice.
Unknown
inv-rconc
[@1: Harry is nice.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "nice" "-")
Fiona is white.
Unknown
rconc
[@1: Fiona is white.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Fiona" "is" "white" "+")
Harry is not rough.
Unknown
inv-random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "-")
Gary is rough.
Unknown
random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "+")
Harry is not smart.
Unknown
inv-random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "-")
Fiona is smart.
Unknown
random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "+")
@0: Anne is rough.[(triple1)] Fiona is nice.[(triple2)] Fiona is not rough.[(triple3)] Gary is blue.[(triple4)] Gary is not white.[(triple5)] Harry is round.[(triple6)] Harry is white.[(triple7)] @1: Anne is nice.[(((triple1) -> rule6))] Fiona is big.[(((triple2) -> rule7))] @2: Anne is big.[(((((triple1) -> rule6)) -> rule7))] Anne is blue.[(((((triple1) -> rule6) triple1) -> rule3) OR ((triple1 ((((((triple1) -> rule6)) -> rule7)) -> rule4)) -> rule2) OR ((((((triple1) -> rule6) ((((((triple1) -> rule6)) -> rule7)) -> rule4)) -> rule5) ((((((triple1) -> rule6) ((((((triple1) -> rule6)) -> rule7)) -> rule4)) -> rule5) ((((triple1) -> rule6)) -> rule7)) -> rule8)) -> rule1))] Fiona is round.[(((((triple2) -> rule7)) -> rule4))] @3: Anne is round.[(((((((triple1) -> rule6)) -> rule7)) -> rule4))] @4: Anne is smart.[(((((triple1) -> rule6) ((((((triple1) -> rule6)) -> rule7)) -> rule4)) -> rule5))] @5: Anne is white.[(((((((triple1) -> rule6) ((((((triple1) -> rule6)) -> rule7)) -> rule4)) -> rule5) ((((triple1) -> rule6)) -> rule7)) -> rule8))]
Anne is rough.
("Anne" "is" "rough" "+")
triple1
Fiona is nice.
("Fiona" "is" "nice" "+")
triple2
Fiona is not rough.
("Fiona" "is" "rough" "-")
triple3
Gary is blue.
("Gary" "is" "blue" "+")
triple4
Gary is not white.
("Gary" "is" "white" "-")
triple5
Harry is round.
("Harry" "is" "round" "+")
triple6
Harry is white.
("Harry" "is" "white" "+")
triple7
Anne is nice.
("Anne" "is" "nice" "+")
((triple1) -> (rule6 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
((triple2) -> (rule7 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
((((triple1) -> (rule6 % int2))) -> (rule7 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
((((triple1) -> (rule6 % int2)) triple1) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
((triple1 ((((((triple1) -> (rule6 % int4))) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Anne is nice.
("Anne" "is" "nice" "+")
int4
((((((triple1) -> (rule6 % int6)) ((((((triple1) -> (rule6 % int6))) -> (rule7 % int5))) -> (rule4 % int4))) -> (rule5 % int3)) ((((((triple1) -> (rule6 % int6)) ((((((triple1) -> (rule6 % int6))) -> (rule7 % int5))) -> (rule4 % int4))) -> (rule5 % int3)) ((((triple1) -> (rule6 % int6))) -> (rule7 % int5))) -> (rule8 % int2))) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is round.
("Anne" "is" "round" "+")
int4
Anne is big.
("Anne" "is" "big" "+")
int5
Anne is nice.
("Anne" "is" "nice" "+")
int6
Fiona is round.
("Fiona" "is" "round" "+")
((((triple2) -> (rule7 % int2))) -> (rule4 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
((((((triple1) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
((((triple1) -> (rule6 % int4)) ((((((triple1) -> (rule6 % int4))) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Anne is nice.
("Anne" "is" "nice" "+")
int4
Anne is white.
("Anne" "is" "white" "+")
((((((triple1) -> (rule6 % int5)) ((((((triple1) -> (rule6 % int5))) -> (rule7 % int4))) -> (rule4 % int3))) -> (rule5 % int2)) ((((triple1) -> (rule6 % int5))) -> (rule7 % int4))) -> (rule8 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Anne is big.
("Anne" "is" "big" "+")
int4
Anne is nice.
("Anne" "is" "nice" "+")
int5