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