Dave is big. Dave is red. Fiona is big. Fiona is not green. Gary is green. Gary is red. Harry is big. Harry is blue. Harry is green. Harry is quiet. Harry is red. Harry is young. Blue people are young. Quiet, red people are young. All red, green people are big. If Gary is big then Gary is blue. Blue, young people are quiet. All young, quiet people are cold. If someone is big and not green then they are red.
Dave is big.
("Dave" "is" "big" "+")
Dave is red.
("Dave" "is" "red" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is not green.
("Fiona" "is" "green" "-")
Gary is green.
("Gary" "is" "green" "+")
Gary is red.
("Gary" "is" "red" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is young.
("Harry" "is" "young" "+")
Blue people are young.
((("someone" "is" "blue" "+")) -> ("someone" "is" "young" "+"))
Quiet, red people are young.
((("someone" "is" "quiet" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "young" "+"))
All red, green people are big.
((("someone" "is" "red" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "big" "+"))
If Gary is big then Gary is blue.
((("Gary" "is" "big" "+")) -> ("Gary" "is" "blue" "+"))
Blue, young people are quiet.
((("someone" "is" "blue" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "quiet" "+"))
All young, quiet people are cold.
((("someone" "is" "young" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "cold" "+"))
If someone is big and not green then they are red.
((("someone" "is" "big" "+") ("someone" "is" "green" "~")) -> ("someone" "is" "red" "+"))
Dave is red.
True
1
proof
[(triple2)]
("Dave" "is" "red" "+")
triple2
Harry is not red.
False
1
inv-proof
[(triple11)]
("Harry" "is" "red" "-")
triple11
Harry is cold.
True
3
proof
[(((triple12 triple10) -> rule6) OR ((triple12 ((triple8 triple12) -> rule5)) -> rule6) OR ((((triple8) -> rule1) triple10) -> rule6) OR ((((triple10 triple11) -> rule2) triple10) -> rule6) OR ((((triple8) -> rule1) ((triple8 triple12) -> rule5)) -> rule6) OR ((((triple10 triple11) -> rule2) ((triple8 triple12) -> rule5)) -> rule6) OR ((triple12 ((triple8 ((triple8) -> rule1)) -> rule5)) -> rule6) OR ((((triple8) -> rule1) ((triple8 ((triple8) -> rule1)) -> rule5)) -> rule6) OR ((((triple10 triple11) -> rule2) ((triple8 ((triple8) -> rule1)) -> rule5)) -> rule6))]
("Harry" "is" "cold" "+")
((triple12 triple10) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
((triple12 ((triple8 triple12) -> (rule5 % int2))) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
((((triple8) -> (rule1 % int2)) triple10) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
((((triple10 triple11) -> (rule2 % int2)) triple10) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
((((triple8) -> (rule1 % int3)) ((triple8 triple12) -> (rule5 % int2))) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
((((triple10 triple11) -> (rule2 % int3)) ((triple8 triple12) -> (rule5 % int2))) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
((triple12 ((triple8 ((triple8) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
((((triple8) -> (rule1 % int3)) ((triple8 ((triple8) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
((((triple10 triple11) -> (rule2 % int3)) ((triple8 ((triple8) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Gary is not big.
False
3
inv-proof
[(((triple6 triple5) -> rule3))]
("Gary" "is" "big" "-")
((triple6 triple5) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is blue.
True
4
proof
[(((((triple6 triple5) -> rule3)) -> rule4))]
("Gary" "is" "blue" "+")
((((triple6 triple5) -> (rule3 % int2))) -> (rule4 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is not blue.
False
4
inv-proof
[(((((triple6 triple5) -> rule3)) -> rule4))]
("Gary" "is" "blue" "-")
((((triple6 triple5) -> (rule3 % int2))) -> (rule4 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is young.
True
5
proof
[(((((((triple6 triple5) -> rule3)) -> rule4)) -> rule1))]
("Gary" "is" "young" "+")
((((((triple6 triple5) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Gary is not young.
False
5
inv-proof
[(((((((triple6 triple5) -> rule3)) -> rule4)) -> rule1))]
("Gary" "is" "young" "-")
((((((triple6 triple5) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Gary is quiet.
True
10
proof
[(((((((triple6 triple5) -> rule3)) -> rule4) ((((((triple6 triple5) -> rule3)) -> rule4)) -> rule1)) -> rule5))]
("Gary" "is" "quiet" "+")
((((((triple6 triple5) -> (rule3 % int4))) -> (rule4 % int3)) ((((((triple6 triple5) -> (rule3 % int4))) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
int4
Gary is not quiet.
False
10
inv-proof
[(((((((triple6 triple5) -> rule3)) -> rule4) ((((((triple6 triple5) -> rule3)) -> rule4)) -> rule1)) -> rule5))]
("Gary" "is" "quiet" "-")
((((((triple6 triple5) -> (rule3 % int4))) -> (rule4 % int3)) ((((((triple6 triple5) -> (rule3 % int4))) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
int4
Gary is cold.
True
16
proof
[(((((((((triple6 triple5) -> rule3)) -> rule4)) -> rule1) ((((((triple6 triple5) -> rule3)) -> rule4) ((((((triple6 triple5) -> rule3)) -> rule4)) -> rule1)) -> rule5)) -> rule6))]
("Gary" "is" "cold" "+")
((((((((triple6 triple5) -> (rule3 % int5))) -> (rule4 % int4))) -> (rule1 % int3)) ((((((triple6 triple5) -> (rule3 % int5))) -> (rule4 % int4)) ((((((triple6 triple5) -> (rule3 % int5))) -> (rule4 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Gary is blue.
("Gary" "is" "blue" "+")
int4
Gary is big.
("Gary" "is" "big" "+")
int5
Gary is not cold.
False
16
inv-proof
[(((((((((triple6 triple5) -> rule3)) -> rule4)) -> rule1) ((((((triple6 triple5) -> rule3)) -> rule4) ((((((triple6 triple5) -> rule3)) -> rule4)) -> rule1)) -> rule5)) -> rule6))]
("Gary" "is" "cold" "-")
((((((((triple6 triple5) -> (rule3 % int5))) -> (rule4 % int4))) -> (rule1 % int3)) ((((((triple6 triple5) -> (rule3 % int5))) -> (rule4 % int4)) ((((((triple6 triple5) -> (rule3 % int5))) -> (rule4 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Gary is blue.
("Gary" "is" "blue" "+")
int4
Gary is big.
("Gary" "is" "big" "+")
int5
Dave is not cold.
Unknown
inv-rconc
[@2: Dave is cold.[CWA. Example of deepest failure = (rule6 <- rule5 <- FAIL)]]
("Dave" "is" "cold" "-")
Fiona is cold.
Unknown
rconc
[@2: Fiona is cold.[CWA. Example of deepest failure = (rule6 <- rule5 <- FAIL)]]
("Fiona" "is" "cold" "+")
Fiona is not quiet.
Unknown
inv-rconc
[@1: Fiona is quiet.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Fiona" "is" "quiet" "-")
Fiona is young.
Unknown
rconc
[@2: Fiona is young.[CWA. Example of deepest failure = (rule2 <- rule5 <- FAIL)]]
("Fiona" "is" "young" "+")
Dave is not quiet.
Unknown
inv-rconc
[@1: Dave is quiet.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Dave" "is" "quiet" "-")
Dave is young.
Unknown
rconc
[@2: Dave is young.[CWA. Example of deepest failure = (rule2 <- rule5 <- FAIL)]]
("Dave" "is" "young" "+")
Fiona is not blue.
Unknown
inv-random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "-")
Dave is green.
Unknown
random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "+")
@0: Dave is big.[(triple1)] Dave is red.[(triple2)] Fiona is big.[(triple3)] Fiona is not green.[(triple4)] Gary is green.[(triple5)] Gary is red.[(triple6)] Harry is big.[(triple7 OR ((triple11 triple9) -> rule3))] Harry is blue.[(triple8)] Harry is green.[(triple9)] Harry is quiet.[(triple10 OR ((triple8 triple12) -> rule5) OR ((triple8 ((triple8) -> rule1)) -> rule5))] Harry is red.[(triple11)] Harry is young.[(triple12 OR ((triple8) -> rule1) OR ((triple10 triple11) -> rule2))] @1: Fiona is red.[(((triple3 triple4) -> rule7))] Gary is big.[(((triple6 triple5) -> rule3))] Harry is cold.[(((triple12 triple10) -> rule6) OR ((triple12 ((triple8 triple12) -> rule5)) -> rule6) OR ((((triple8) -> rule1) triple10) -> rule6) OR ((((triple10 triple11) -> rule2) triple10) -> rule6) OR ((((triple8) -> rule1) ((triple8 triple12) -> rule5)) -> rule6) OR ((((triple10 triple11) -> rule2) ((triple8 triple12) -> rule5)) -> rule6) OR ((triple12 ((triple8 ((triple8) -> rule1)) -> rule5)) -> rule6) OR ((((triple8) -> rule1) ((triple8 ((triple8) -> rule1)) -> rule5)) -> rule6) OR ((((triple10 triple11) -> rule2) ((triple8 ((triple8) -> rule1)) -> rule5)) -> rule6))] @2: Gary is blue.[(((((triple6 triple5) -> rule3)) -> rule4))] @3: Gary is young.[(((((((triple6 triple5) -> rule3)) -> rule4)) -> rule1))] @4: Gary is quiet.[(((((((triple6 triple5) -> rule3)) -> rule4) ((((((triple6 triple5) -> rule3)) -> rule4)) -> rule1)) -> rule5))] @5: Gary is cold.[(((((((((triple6 triple5) -> rule3)) -> rule4)) -> rule1) ((((((triple6 triple5) -> rule3)) -> rule4) ((((((triple6 triple5) -> rule3)) -> rule4)) -> rule1)) -> rule5)) -> rule6))]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is red.
("Dave" "is" "red" "+")
triple2
Fiona is big.
("Fiona" "is" "big" "+")
triple3
Fiona is not green.
("Fiona" "is" "green" "-")
triple4
Gary is green.
("Gary" "is" "green" "+")
triple5
Gary is red.
("Gary" "is" "red" "+")
triple6
Harry is big.
("Harry" "is" "big" "+")
triple7
((triple11 triple9) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
triple8
Harry is green.
("Harry" "is" "green" "+")
triple9
Harry is quiet.
("Harry" "is" "quiet" "+")
triple10
((triple8 triple12) -> (rule5 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((triple8 ((triple8) -> (rule1 % int2))) -> (rule5 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
triple11
Harry is young.
("Harry" "is" "young" "+")
triple12
((triple8) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
((triple10 triple11) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
((triple3 triple4) -> (rule7 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
((triple6 triple5) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
((triple12 triple10) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
((triple12 ((triple8 triple12) -> (rule5 % int2))) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
((((triple8) -> (rule1 % int2)) triple10) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
((((triple10 triple11) -> (rule2 % int2)) triple10) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
((((triple8) -> (rule1 % int3)) ((triple8 triple12) -> (rule5 % int2))) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
((((triple10 triple11) -> (rule2 % int3)) ((triple8 triple12) -> (rule5 % int2))) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
((triple12 ((triple8 ((triple8) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
((((triple8) -> (rule1 % int3)) ((triple8 ((triple8) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
((((triple10 triple11) -> (rule2 % int3)) ((triple8 ((triple8) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Gary is blue.
("Gary" "is" "blue" "+")
((((triple6 triple5) -> (rule3 % int2))) -> (rule4 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
((((((triple6 triple5) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
((((((triple6 triple5) -> (rule3 % int4))) -> (rule4 % int3)) ((((((triple6 triple5) -> (rule3 % int4))) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
int4
Gary is cold.
("Gary" "is" "cold" "+")
((((((((triple6 triple5) -> (rule3 % int5))) -> (rule4 % int4))) -> (rule1 % int3)) ((((((triple6 triple5) -> (rule3 % int5))) -> (rule4 % int4)) ((((((triple6 triple5) -> (rule3 % int5))) -> (rule4 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Gary is blue.
("Gary" "is" "blue" "+")
int4
Gary is big.
("Gary" "is" "big" "+")
int5