Anne is green. Anne is quiet. Anne is rough. Anne is smart. Bob is quiet. Bob is round. Bob is young. Charlie is green. Charlie is red. Fiona is rough. Rough people are quiet. If someone is young and green then they are smart. Green, smart people are young. All young, green people are quiet. If Fiona is quiet and Fiona is young then Fiona is red. All rough people are smart. If someone is rough and young then they are round. Red, rough people are quiet.
Anne is green.
("Anne" "is" "green" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is young.
("Bob" "is" "young" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Rough people are quiet.
((("someone" "is" "rough" "+")) -> ("someone" "is" "quiet" "+"))
If someone is young and green then they are smart.
((("someone" "is" "young" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "smart" "+"))
Green, smart people are young.
((("someone" "is" "green" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "young" "+"))
All young, green people are quiet.
((("someone" "is" "young" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "quiet" "+"))
If Fiona is quiet and Fiona is young then Fiona is red.
((("Fiona" "is" "quiet" "+") ("Fiona" "is" "young" "+")) -> ("Fiona" "is" "red" "+"))
All rough people are smart.
((("someone" "is" "rough" "+")) -> ("someone" "is" "smart" "+"))
If someone is rough and young then they are round.
((("someone" "is" "rough" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "round" "+"))
Red, rough people are quiet.
((("someone" "is" "red" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "quiet" "+"))
Bob is young.
True
1
proof
[(triple7)]
("Bob" "is" "young" "+")
triple7
Anne is not green.
False
1
inv-proof
[(triple1)]
("Anne" "is" "green" "-")
triple1
Fiona is quiet.
True
2
proof
[(((triple10) -> rule1))]
("Fiona" "is" "quiet" "+")
((triple10) -> (rule1 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is not smart.
False
2
inv-proof
[(((triple10) -> rule6))]
("Fiona" "is" "smart" "-")
((triple10) -> (rule6 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Anne is round.
True
5
proof
[(((triple3 ((triple1 triple4) -> rule3)) -> rule7) OR ((triple3 ((triple1 ((triple3) -> rule6)) -> rule3)) -> rule7))]
("Anne" "is" "round" "+")
((triple3 ((triple1 triple4) -> (rule3 % int2))) -> (rule7 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
((triple3 ((triple1 ((triple3) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is not round.
False
5
inv-proof
[(((triple3 ((triple1 triple4) -> rule3)) -> rule7) OR ((triple3 ((triple1 ((triple3) -> rule6)) -> rule3)) -> rule7))]
("Anne" "is" "round" "-")
((triple3 ((triple1 triple4) -> (rule3 % int2))) -> (rule7 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
((triple3 ((triple1 ((triple3) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Charlie is not young.
Unknown
inv-rconc
[@2: Charlie is young.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("Charlie" "is" "young" "-")
Charlie is quiet.
Unknown
rconc
[@3: Charlie is quiet.[CWA. Example of deepest failure = (rule4 <- rule3 <- rule2 <- FAIL)]]
("Charlie" "is" "quiet" "+")
Charlie is not smart.
Unknown
inv-rconc
[@3: Charlie is smart.[CWA. Example of deepest failure = (rule2 <- rule3 <- rule6 <- FAIL)]]
("Charlie" "is" "smart" "-")
Bob is red.
Unknown
random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "+")
Anne is not red.
Unknown
inv-random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "-")
Charlie is rough.
Unknown
random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "+")
@0: Anne is green.[(triple1)] Anne is quiet.[(triple2 OR ((triple3) -> rule1) OR ((((triple1 triple4) -> rule3) triple1) -> rule4) OR ((((triple1 ((triple3) -> rule6)) -> rule3) triple1) -> rule4))] Anne is rough.[(triple3)] Anne is smart.[(triple4 OR ((triple3) -> rule6))] Bob is quiet.[(triple5)] Bob is round.[(triple6)] Bob is young.[(triple7)] Charlie is green.[(triple8)] Charlie is red.[(triple9)] Fiona is rough.[(triple10)] @1: Anne is young.[(((triple1 triple4) -> rule3) OR ((triple1 ((triple3) -> rule6)) -> rule3))] Fiona is quiet.[(((triple10) -> rule1))] Fiona is smart.[(((triple10) -> rule6))] @2: Anne is round.[(((triple3 ((triple1 triple4) -> rule3)) -> rule7) OR ((triple3 ((triple1 ((triple3) -> rule6)) -> rule3)) -> rule7))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
((triple3) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
((((triple1 triple4) -> (rule3 % int2)) triple1) -> (rule4 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
((((triple1 ((triple3) -> (rule6 % int3))) -> (rule3 % int2)) triple1) -> (rule4 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is rough.
("Anne" "is" "rough" "+")
triple3
Anne is smart.
("Anne" "is" "smart" "+")
triple4
((triple3) -> (rule6 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple5
Bob is round.
("Bob" "is" "round" "+")
triple6
Bob is young.
("Bob" "is" "young" "+")
triple7
Charlie is green.
("Charlie" "is" "green" "+")
triple8
Charlie is red.
("Charlie" "is" "red" "+")
triple9
Fiona is rough.
("Fiona" "is" "rough" "+")
triple10
Anne is young.
("Anne" "is" "young" "+")
((triple1 triple4) -> (rule3 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
((triple1 ((triple3) -> (rule6 % int2))) -> (rule3 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((triple10) -> (rule1 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
((triple10) -> (rule6 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
((triple3 ((triple1 triple4) -> (rule3 % int2))) -> (rule7 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
((triple3 ((triple1 ((triple3) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3