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