Dave is blue. Dave is green. Dave is rough. Dave is young. Erin is blue. Erin is furry. Erin is green. Erin is quiet. Erin is young. Fiona is furry. Fiona is young. Gary is big. Gary is furry. Gary is green. Gary is young. If Fiona is quiet and Fiona is blue then Fiona is furry. All rough things are quiet. If something is young then it is green. If something is blue and big then it is green. Green, big things are blue. If something is big then it is rough. All young things are green. All furry, blue things are quiet.
Dave is blue.
("Dave" "is" "blue" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is young.
("Dave" "is" "young" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is young.
("Erin" "is" "young" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is young.
("Gary" "is" "young" "+")
If Fiona is quiet and Fiona is blue then Fiona is furry.
((("Fiona" "is" "quiet" "+") ("Fiona" "is" "blue" "+")) -> ("Fiona" "is" "furry" "+"))
All rough things are quiet.
((("something" "is" "rough" "+")) -> ("something" "is" "quiet" "+"))
If something is young then it is green.
((("something" "is" "young" "+")) -> ("something" "is" "green" "+"))
If something is blue and big then it is green.
((("something" "is" "blue" "+") ("something" "is" "big" "+")) -> ("something" "is" "green" "+"))
Green, big things are blue.
((("something" "is" "green" "+") ("something" "is" "big" "+")) -> ("something" "is" "blue" "+"))
If something is big then it is rough.
((("something" "is" "big" "+")) -> ("something" "is" "rough" "+"))
All young things are green.
((("something" "is" "young" "+")) -> ("something" "is" "green" "+"))
All furry, blue things are quiet.
((("something" "is" "furry" "+") ("something" "is" "blue" "+")) -> ("something" "is" "quiet" "+"))
Gary is big.
True
1
proof
[(triple12)]
("Gary" "is" "big" "+")
triple12
Gary is not young.
False
1
inv-proof
[(triple15)]
("Gary" "is" "young" "-")
triple15
Fiona is green.
True
2
proof
[(((triple11) -> rule3) OR ((triple11) -> rule7))]
("Fiona" "is" "green" "+")
((triple11) -> (rule3 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
((triple11) -> (rule7 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Dave is not quiet.
False
2
inv-proof
[(((triple3) -> rule2))]
("Dave" "is" "quiet" "-")
((triple3) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Gary is quiet.
True
3
proof
[(((((triple12) -> rule6)) -> rule2) OR ((triple13 ((triple14 triple12) -> rule5)) -> rule8) OR ((triple13 ((((triple15) -> rule3) triple12) -> rule5)) -> rule8) OR ((triple13 ((((triple15) -> rule7) triple12) -> rule5)) -> rule8))]
("Gary" "is" "quiet" "+")
((((triple12) -> (rule6 % int2))) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
((triple13 ((triple14 triple12) -> (rule5 % int2))) -> (rule8 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
((triple13 ((((triple15) -> (rule3 % int3)) triple12) -> (rule5 % int2))) -> (rule8 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
((triple13 ((((triple15) -> (rule7 % int3)) triple12) -> (rule5 % int2))) -> (rule8 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Gary is not quiet.
False
3
inv-proof
[(((((triple12) -> rule6)) -> rule2) OR ((triple13 ((triple14 triple12) -> rule5)) -> rule8) OR ((triple13 ((((triple15) -> rule3) triple12) -> rule5)) -> rule8) OR ((triple13 ((((triple15) -> rule7) triple12) -> rule5)) -> rule8))]
("Gary" "is" "quiet" "-")
((((triple12) -> (rule6 % int2))) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
((triple13 ((triple14 triple12) -> (rule5 % int2))) -> (rule8 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
((triple13 ((((triple15) -> (rule3 % int3)) triple12) -> (rule5 % int2))) -> (rule8 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
((triple13 ((((triple15) -> (rule7 % int3)) triple12) -> (rule5 % int2))) -> (rule8 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Fiona is not blue.
Unknown
inv-rconc
[@1: Fiona is blue.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Fiona" "is" "blue" "-")
Erin is rough.
Unknown
rconc
[@1: Erin is rough.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Erin" "is" "rough" "+")
Fiona is not quiet.
Unknown
inv-rconc
[@2: Fiona is quiet.[CWA. Example of deepest failure = (rule2 <- rule6 <- FAIL)]]
("Fiona" "is" "quiet" "-")
Erin is big.
Unknown
random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "+")
Fiona is not big.
Unknown
inv-random
[@0: Fiona is big.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "big" "-")
Dave is big.
Unknown
random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "+")
@0: Dave is blue.[(triple1)] Dave is green.[(triple2 OR ((triple4) -> rule3) OR ((triple4) -> rule7))] Dave is rough.[(triple3)] Dave is young.[(triple4)] Erin is blue.[(triple5)] Erin is furry.[(triple6)] Erin is green.[(triple7 OR ((triple9) -> rule3) OR ((triple9) -> rule7))] Erin is quiet.[(triple8 OR ((triple6 triple5) -> rule8))] Erin is young.[(triple9)] Fiona is furry.[(triple10)] Fiona is young.[(triple11)] Gary is big.[(triple12)] Gary is furry.[(triple13)] Gary is green.[(triple14 OR ((triple15) -> rule3) OR ((triple15) -> rule7))] Gary is young.[(triple15)] @1: Dave is quiet.[(((triple3) -> rule2))] Fiona is green.[(((triple11) -> rule3) OR ((triple11) -> rule7))] Gary is blue.[(((triple14 triple12) -> rule5) OR ((((triple15) -> rule3) triple12) -> rule5) OR ((((triple15) -> rule7) triple12) -> rule5))] Gary is rough.[(((triple12) -> rule6))] @2: Gary is quiet.[(((((triple12) -> rule6)) -> rule2) OR ((triple13 ((triple14 triple12) -> rule5)) -> rule8) OR ((triple13 ((((triple15) -> rule3) triple12) -> rule5)) -> rule8) OR ((triple13 ((((triple15) -> rule7) triple12) -> rule5)) -> rule8))]
Dave is blue.
("Dave" "is" "blue" "+")
triple1
Dave is green.
("Dave" "is" "green" "+")
triple2
((triple4) -> (rule3 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((triple4) -> (rule7 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
triple3
Dave is young.
("Dave" "is" "young" "+")
triple4
Erin is blue.
("Erin" "is" "blue" "+")
triple5
Erin is furry.
("Erin" "is" "furry" "+")
triple6
Erin is green.
("Erin" "is" "green" "+")
triple7
((triple9) -> (rule3 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
((triple9) -> (rule7 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
triple8
((triple6 triple5) -> (rule8 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
triple9
Fiona is furry.
("Fiona" "is" "furry" "+")
triple10
Fiona is young.
("Fiona" "is" "young" "+")
triple11
Gary is big.
("Gary" "is" "big" "+")
triple12
Gary is furry.
("Gary" "is" "furry" "+")
triple13
Gary is green.
("Gary" "is" "green" "+")
triple14
((triple15) -> (rule3 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((triple15) -> (rule7 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
triple15
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple3) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
((triple11) -> (rule3 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
((triple11) -> (rule7 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
((triple14 triple12) -> (rule5 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
((((triple15) -> (rule3 % int2)) triple12) -> (rule5 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
((((triple15) -> (rule7 % int2)) triple12) -> (rule5 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
((triple12) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
((((triple12) -> (rule6 % int2))) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
((triple13 ((triple14 triple12) -> (rule5 % int2))) -> (rule8 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
((triple13 ((((triple15) -> (rule3 % int3)) triple12) -> (rule5 % int2))) -> (rule8 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
((triple13 ((((triple15) -> (rule7 % int3)) triple12) -> (rule5 % int2))) -> (rule8 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3