Anne is rough. Anne is round. Charlie is round. Fiona is rough. Gary is quiet. Gary is rough. Gary is young. If someone is big then they are blue. If someone is round and rough then they are blue. If someone is quiet then they are young. If Fiona is rough then Fiona is big. Round, blue people are big. If someone is round and big then they are quiet. If Gary is blue and Gary is young then Gary is not quiet. Young people are not green. If someone is rough and not young then they are not green.
Anne is rough.
("Anne" "is" "rough" "+")
Anne is round.
("Anne" "is" "round" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is young.
("Gary" "is" "young" "+")
If someone is big then they are blue.
((("someone" "is" "big" "+")) -> ("someone" "is" "blue" "+"))
If someone is round and rough then they are blue.
((("someone" "is" "round" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "blue" "+"))
If someone is quiet then they are young.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "young" "+"))
If Fiona is rough then Fiona is big.
((("Fiona" "is" "rough" "+")) -> ("Fiona" "is" "big" "+"))
Round, blue people are big.
((("someone" "is" "round" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "big" "+"))
If someone is round and big then they are quiet.
((("someone" "is" "round" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "quiet" "+"))
If Gary is blue and Gary is young then Gary is not quiet.
((("Gary" "is" "blue" "+") ("Gary" "is" "young" "+")) -> ("Gary" "is" "quiet" "-"))
Young people are not green.
((("someone" "is" "young" "+")) -> ("someone" "is" "green" "-"))
If someone is rough and not young then they are not green.
((("someone" "is" "rough" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "green" "-"))
Gary is young.
True
1
proof
[(triple7 OR ((triple5) -> rule3))]
("Gary" "is" "young" "+")
triple7
((triple5) -> (rule3 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Anne is not rough.
False
1
inv-proof
[(triple1)]
("Anne" "is" "rough" "-")
triple1
Anne is blue.
True
3
proof
[(((triple2 triple1) -> rule2))]
("Anne" "is" "blue" "+")
((triple2 triple1) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Gary is green.
False
2
inv-proof
[(((triple7) -> rule8) OR ((((triple5) -> rule3)) -> rule8))]
("Gary" "is" "green" "+")
((triple7) -> (rule8 % int1))
Gary is not green.
("Gary" "is" "green" "-")
int1
((((triple5) -> (rule3 % int2))) -> (rule8 % int1))
Gary is not green.
("Gary" "is" "green" "-")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Fiona is blue.
True
3
proof
[(((((triple4) -> rule4)) -> rule1))]
("Fiona" "is" "blue" "+")
((((triple4) -> (rule4 % int2))) -> (rule1 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is not blue.
False
3
inv-proof
[(((((triple4) -> rule4)) -> rule1))]
("Fiona" "is" "blue" "-")
((((triple4) -> (rule4 % int2))) -> (rule1 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Anne is quiet.
True
7
proof
[(((triple2 ((triple2 ((triple2 triple1) -> rule2)) -> rule5)) -> rule6))]
("Anne" "is" "quiet" "+")
((triple2 ((triple2 ((triple2 triple1) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Anne is not quiet.
False
7
inv-proof
[(((triple2 ((triple2 ((triple2 triple1) -> rule2)) -> rule5)) -> rule6))]
("Anne" "is" "quiet" "-")
((triple2 ((triple2 ((triple2 triple1) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Anne is young.
True
8
proof
[(((((triple2 ((triple2 ((triple2 triple1) -> rule2)) -> rule5)) -> rule6)) -> rule3))]
("Anne" "is" "young" "+")
((((triple2 ((triple2 ((triple2 triple1) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Anne is blue.
("Anne" "is" "blue" "+")
int4
Anne is not young.
False
8
inv-proof
[(((((triple2 ((triple2 ((triple2 triple1) -> rule2)) -> rule5)) -> rule6)) -> rule3))]
("Anne" "is" "young" "-")
((((triple2 ((triple2 ((triple2 triple1) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Anne is blue.
("Anne" "is" "blue" "+")
int4
Anne is not green.
True
9
proof
[(((((((triple2 ((triple2 ((triple2 triple1) -> rule2)) -> rule5)) -> rule6)) -> rule3)) -> rule8))]
("Anne" "is" "green" "-")
((((((triple2 ((triple2 ((triple2 triple1) -> (rule2 % int5))) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Anne is not green.
("Anne" "is" "green" "-")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Anne is big.
("Anne" "is" "big" "+")
int4
Anne is blue.
("Anne" "is" "blue" "+")
int5
Anne is green.
False
9
inv-proof
[(((((((triple2 ((triple2 ((triple2 triple1) -> rule2)) -> rule5)) -> rule6)) -> rule3)) -> rule8))]
("Anne" "is" "green" "+")
((((((triple2 ((triple2 ((triple2 triple1) -> (rule2 % int5))) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Anne is not green.
("Anne" "is" "green" "-")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Anne is big.
("Anne" "is" "big" "+")
int4
Anne is blue.
("Anne" "is" "blue" "+")
int5
Charlie is not young.
Unknown
inv-rconc
[@4: Charlie is young.[CWA. Example of deepest failure = (rule3 <- rule6 <- rule5 <- rule1 <- FAIL)]]
("Charlie" "is" "young" "-")
Charlie is big.
Unknown
rconc
[@2: Charlie is big.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("Charlie" "is" "big" "+")
Fiona is not young.
Unknown
inv-rconc
[@2: Fiona is young.[CWA. Example of deepest failure = (rule3 <- rule6 <- FAIL)]]
("Fiona" "is" "young" "-")
Gary is blue.
Unknown
rconc
[@2: Gary is blue.[CWA. Example of deepest failure = (rule1 <- rule5 <- FAIL)]]
("Gary" "is" "blue" "+")
Charlie is not blue.
Unknown
inv-rconc
[@3: Charlie is blue.[CWA. Example of deepest failure = (rule1 <- rule5 <- rule2 <- FAIL)]]
("Charlie" "is" "blue" "-")
Fiona is quiet.
Unknown
rconc
[@1: Fiona is quiet.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Fiona" "is" "quiet" "+")
Fiona is not round.
Unknown
inv-random
[@0: Fiona is round.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "round" "-")
Charlie is rough.
Unknown
random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "+")
Charlie is not green.
Unknown
inv-random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "-")
Fiona is green.
Unknown
random
[@0: Fiona is green.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "green" "+")
@0: Anne is rough.[(triple1)] Anne is round.[(triple2)] Charlie is round.[(triple3)] Fiona is rough.[(triple4)] Gary is quiet.[(triple5)] Gary is rough.[(triple6)] Gary is young.[(triple7 OR ((triple5) -> rule3))] @1: Anne is blue.[(((triple2 triple1) -> rule2))] Fiona is big.[(((triple4) -> rule4))] Gary is not green.[(((triple7) -> rule8) OR ((((triple5) -> rule3)) -> rule8))] @2: Anne is big.[(((triple2 ((triple2 triple1) -> rule2)) -> rule5))] Fiona is blue.[(((((triple4) -> rule4)) -> rule1))] @3: Anne is quiet.[(((triple2 ((triple2 ((triple2 triple1) -> rule2)) -> rule5)) -> rule6))] @4: Anne is young.[(((((triple2 ((triple2 ((triple2 triple1) -> rule2)) -> rule5)) -> rule6)) -> rule3))] @5: Anne is not green.[(((((((triple2 ((triple2 ((triple2 triple1) -> rule2)) -> rule5)) -> rule6)) -> rule3)) -> rule8))]
Anne is rough.
("Anne" "is" "rough" "+")
triple1
Anne is round.
("Anne" "is" "round" "+")
triple2
Charlie is round.
("Charlie" "is" "round" "+")
triple3
Fiona is rough.
("Fiona" "is" "rough" "+")
triple4
Gary is quiet.
("Gary" "is" "quiet" "+")
triple5
Gary is rough.
("Gary" "is" "rough" "+")
triple6
Gary is young.
("Gary" "is" "young" "+")
triple7
((triple5) -> (rule3 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
((triple2 triple1) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
((triple4) -> (rule4 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Gary is not green.
("Gary" "is" "green" "-")
((triple7) -> (rule8 % int1))
Gary is not green.
("Gary" "is" "green" "-")
int1
((((triple5) -> (rule3 % int2))) -> (rule8 % int1))
Gary is not green.
("Gary" "is" "green" "-")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
((triple2 ((triple2 triple1) -> (rule2 % int2))) -> (rule5 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
((((triple4) -> (rule4 % int2))) -> (rule1 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple2 ((triple2 ((triple2 triple1) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
((((triple2 ((triple2 ((triple2 triple1) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Anne is blue.
("Anne" "is" "blue" "+")
int4
Anne is not green.
("Anne" "is" "green" "-")
((((((triple2 ((triple2 ((triple2 triple1) -> (rule2 % int5))) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Anne is not green.
("Anne" "is" "green" "-")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Anne is big.
("Anne" "is" "big" "+")
int4
Anne is blue.
("Anne" "is" "blue" "+")
int5