Anne is big. Anne is cold. Anne is nice. Charlie is big. Charlie is cold. Charlie is nice. Charlie is red. Charlie is round. Charlie is smart. Charlie is white. Dave is round. Fiona is big. Smart people are big. If Dave is big then Dave is nice. Round people are smart. If someone is red and nice then they are white. All smart, red people are round. All round, white people are red. If someone is nice then they are red. If Charlie is cold then Charlie is round.
Anne is big.
("Anne" "is" "big" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Dave is round.
("Dave" "is" "round" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Smart people are big.
((("someone" "is" "smart" "+")) -> ("someone" "is" "big" "+"))
If Dave is big then Dave is nice.
((("Dave" "is" "big" "+")) -> ("Dave" "is" "nice" "+"))
Round people are smart.
((("someone" "is" "round" "+")) -> ("someone" "is" "smart" "+"))
If someone is red and nice then they are white.
((("someone" "is" "red" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "white" "+"))
All smart, red people are round.
((("someone" "is" "smart" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "round" "+"))
All round, white people are red.
((("someone" "is" "round" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "red" "+"))
If someone is nice then they are red.
((("someone" "is" "nice" "+")) -> ("someone" "is" "red" "+"))
If Charlie is cold then Charlie is round.
((("Charlie" "is" "cold" "+")) -> ("Charlie" "is" "round" "+"))
Anne is big.
True
1
proof
[(triple1)]
("Anne" "is" "big" "+")
triple1
Anne is not cold.
False
1
inv-proof
[(triple2)]
("Anne" "is" "cold" "-")
triple2
Dave is smart.
True
2
proof
[(((triple11) -> rule3))]
("Dave" "is" "smart" "+")
((triple11) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Anne is not red.
False
2
inv-proof
[(((triple3) -> rule7))]
("Anne" "is" "red" "-")
((triple3) -> (rule7 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Dave is big.
True
3
proof
[(((((triple11) -> rule3)) -> rule1))]
("Dave" "is" "big" "+")
((((triple11) -> (rule3 % int2))) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is not big.
False
3
inv-proof
[(((((triple11) -> rule3)) -> rule1))]
("Dave" "is" "big" "-")
((((triple11) -> (rule3 % int2))) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is nice.
True
4
proof
[(((((((triple11) -> rule3)) -> rule1)) -> rule2))]
("Dave" "is" "nice" "+")
((((((triple11) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is not nice.
False
4
inv-proof
[(((((((triple11) -> rule3)) -> rule1)) -> rule2))]
("Dave" "is" "nice" "-")
((((((triple11) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is red.
True
5
proof
[(((((((((triple11) -> rule3)) -> rule1)) -> rule2)) -> rule7))]
("Dave" "is" "red" "+")
((((((((triple11) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
int4
Dave is not red.
False
5
inv-proof
[(((((((((triple11) -> rule3)) -> rule1)) -> rule2)) -> rule7))]
("Dave" "is" "red" "-")
((((((((triple11) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
int4
Dave is white.
True
10
proof
[(((((((((((triple11) -> rule3)) -> rule1)) -> rule2)) -> rule7) ((((((triple11) -> rule3)) -> rule1)) -> rule2)) -> rule4))]
("Dave" "is" "white" "+")
((((((((((triple11) -> (rule3 % int5))) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule7 % int2)) ((((((triple11) -> (rule3 % int5))) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule4 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is big.
("Dave" "is" "big" "+")
int4
Dave is smart.
("Dave" "is" "smart" "+")
int5
Dave is not white.
False
10
inv-proof
[(((((((((((triple11) -> rule3)) -> rule1)) -> rule2)) -> rule7) ((((((triple11) -> rule3)) -> rule1)) -> rule2)) -> rule4))]
("Dave" "is" "white" "-")
((((((((((triple11) -> (rule3 % int5))) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule7 % int2)) ((((((triple11) -> (rule3 % int5))) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule4 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is big.
("Dave" "is" "big" "+")
int4
Dave is smart.
("Dave" "is" "smart" "+")
int5
Fiona is not smart.
Unknown
inv-rconc
[@2: Fiona is smart.[CWA. Example of deepest failure = (rule3 <- rule5 <- FAIL)]]
("Fiona" "is" "smart" "-")
Anne is smart.
Unknown
rconc
[@2: Anne is smart.[CWA. Example of deepest failure = (rule3 <- rule5 <- FAIL)]]
("Anne" "is" "smart" "+")
Fiona is not white.
Unknown
inv-rconc
[@1: Fiona is white.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Fiona" "is" "white" "-")
Anne is round.
Unknown
rconc
[@2: Anne is round.[CWA. Example of deepest failure = (rule5 <- rule3 <- FAIL)]]
("Anne" "is" "round" "+")
Fiona is not round.
Unknown
inv-rconc
[@2: Fiona is round.[CWA. Example of deepest failure = (rule5 <- rule3 <- FAIL)]]
("Fiona" "is" "round" "-")
Fiona is red.
Unknown
rconc
[@2: Fiona is red.[CWA. Example of deepest failure = (rule6 <- rule4 <- FAIL)]]
("Fiona" "is" "red" "+")
Dave is not cold.
Unknown
inv-random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "-")
Fiona is cold.
Unknown
random
[@0: Fiona is cold.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "cold" "+")
@0: Anne is big.[(triple1)] Anne is cold.[(triple2)] Anne is nice.[(triple3)] Charlie is big.[(triple4 OR ((triple9) -> rule1) OR ((((triple8) -> rule3)) -> rule1) OR ((((((triple5) -> rule8)) -> rule3)) -> rule1))] Charlie is cold.[(triple5)] Charlie is nice.[(triple6)] Charlie is red.[(triple7 OR ((triple6) -> rule7) OR ((triple8 triple10) -> rule6) OR ((((triple5) -> rule8) triple10) -> rule6))] Charlie is round.[(triple8 OR ((triple5) -> rule8) OR ((triple9 triple7) -> rule5) OR ((triple9 ((triple6) -> rule7)) -> rule5))] Charlie is smart.[(triple9 OR ((triple8) -> rule3) OR ((((triple5) -> rule8)) -> rule3))] Charlie is white.[(triple10 OR ((triple7 triple6) -> rule4) OR ((((triple6) -> rule7) triple6) -> rule4))] Dave is round.[(triple11)] Fiona is big.[(triple12)] @1: Anne is red.[(((triple3) -> rule7))] Dave is smart.[(((triple11) -> rule3))] @2: Anne is white.[(((((triple3) -> rule7) triple3) -> rule4))] Dave is big.[(((((triple11) -> rule3)) -> rule1))] @3: Dave is nice.[(((((((triple11) -> rule3)) -> rule1)) -> rule2))] @4: Dave is red.[(((((((((triple11) -> rule3)) -> rule1)) -> rule2)) -> rule7))] @5: Dave is white.[(((((((((((triple11) -> rule3)) -> rule1)) -> rule2)) -> rule7) ((((((triple11) -> rule3)) -> rule1)) -> rule2)) -> rule4))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is cold.
("Anne" "is" "cold" "+")
triple2
Anne is nice.
("Anne" "is" "nice" "+")
triple3
Charlie is big.
("Charlie" "is" "big" "+")
triple4
((triple9) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((((triple8) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
((((((triple5) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is cold.
("Charlie" "is" "cold" "+")
triple5
Charlie is nice.
("Charlie" "is" "nice" "+")
triple6
Charlie is red.
("Charlie" "is" "red" "+")
triple7
((triple6) -> (rule7 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
((triple8 triple10) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
((((triple5) -> (rule8 % int2)) triple10) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
triple8
((triple5) -> (rule8 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
((triple9 triple7) -> (rule5 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
((triple9 ((triple6) -> (rule7 % int2))) -> (rule5 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
triple9
((triple8) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
((((triple5) -> (rule8 % int2))) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
triple10
((triple7 triple6) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
((((triple6) -> (rule7 % int2)) triple6) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
triple11
Fiona is big.
("Fiona" "is" "big" "+")
triple12
Anne is red.
("Anne" "is" "red" "+")
((triple3) -> (rule7 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
((triple11) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
((((triple3) -> (rule7 % int2)) triple3) -> (rule4 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
((((triple11) -> (rule3 % int2))) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
((((((triple11) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is red.
("Dave" "is" "red" "+")
((((((((triple11) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
int4
Dave is white.
("Dave" "is" "white" "+")
((((((((((triple11) -> (rule3 % int5))) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule7 % int2)) ((((((triple11) -> (rule3 % int5))) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule4 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is big.
("Dave" "is" "big" "+")
int4
Dave is smart.
("Dave" "is" "smart" "+")
int5