Anne is cold. Anne is green. Anne is kind. Anne is quiet. Anne is smart. Charlie is cold. Charlie is green. Charlie is kind. Dave is cold. Dave is young. If someone is young then they are quiet. Kind people are smart. Kind people are nice. Cold, green people are smart. If someone is nice then they are kind. If someone is kind and quiet then they are smart. All nice people are cold. If someone is nice and cold then they are green.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is young.
("Dave" "is" "young" "+")
If someone is young then they are quiet.
((("someone" "is" "young" "+")) -> ("someone" "is" "quiet" "+"))
Kind people are smart.
((("someone" "is" "kind" "+")) -> ("someone" "is" "smart" "+"))
Kind people are nice.
((("someone" "is" "kind" "+")) -> ("someone" "is" "nice" "+"))
Cold, green people are smart.
((("someone" "is" "cold" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "smart" "+"))
If someone is nice then they are kind.
((("someone" "is" "nice" "+")) -> ("someone" "is" "kind" "+"))
If someone is kind and quiet then they are smart.
((("someone" "is" "kind" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "smart" "+"))
All nice people are cold.
((("someone" "is" "nice" "+")) -> ("someone" "is" "cold" "+"))
If someone is nice and cold then they are green.
((("someone" "is" "nice" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "green" "+"))
Dave is cold.
True
1
proof
[(triple9)]
("Dave" "is" "cold" "+")
triple9
Anne is not quiet.
False
1
inv-proof
[(triple4)]
("Anne" "is" "quiet" "-")
triple4
Dave is not kind.
Unknown
inv-rconc
[@2: Dave is kind.[CWA. Example of deepest failure = (rule5 <- rule3 <- FAIL)]]
("Dave" "is" "kind" "-")
Charlie is young.
Unknown
random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "+")
@0: Anne is cold.[(triple1 OR ((((triple3) -> rule3)) -> rule7))] Anne is green.[(triple2 OR ((((triple3) -> rule3) triple1) -> rule8) OR ((((triple3) -> rule3) ((((triple3) -> rule3)) -> rule7)) -> rule8))] Anne is kind.[(triple3)] Anne is quiet.[(triple4)] Anne is smart.[(triple5 OR ((triple3) -> rule2) OR ((triple1 triple2) -> rule4) OR ((triple3 triple4) -> rule6) OR ((triple1 ((((triple3) -> rule3) triple1) -> rule8)) -> rule4) OR ((((((triple3) -> rule3)) -> rule7) triple2) -> rule4) OR ((((((triple3) -> rule3)) -> rule7) ((((triple3) -> rule3) triple1) -> rule8)) -> rule4) OR ((triple1 ((((triple3) -> rule3) ((((triple3) -> rule3)) -> rule7)) -> rule8)) -> rule4) OR ((((((triple3) -> rule3)) -> rule7) ((((triple3) -> rule3) ((((triple3) -> rule3)) -> rule7)) -> rule8)) -> rule4))] Charlie is cold.[(triple6 OR ((((triple8) -> rule3)) -> rule7))] Charlie is green.[(triple7 OR ((((triple8) -> rule3) triple6) -> rule8) OR ((((triple8) -> rule3) ((((triple8) -> rule3)) -> rule7)) -> rule8))] Charlie is kind.[(triple8)] Dave is cold.[(triple9)] Dave is young.[(triple10)] @1: Anne is nice.[(((triple3) -> rule3))] Charlie is nice.[(((triple8) -> rule3))] Charlie is smart.[(((triple8) -> rule2) OR ((triple6 triple7) -> rule4) OR ((triple6 ((((triple8) -> rule3) triple6) -> rule8)) -> rule4) OR ((((((triple8) -> rule3)) -> rule7) triple7) -> rule4) OR ((((((triple8) -> rule3)) -> rule7) ((((triple8) -> rule3) triple6) -> rule8)) -> rule4) OR ((triple6 ((((triple8) -> rule3) ((((triple8) -> rule3)) -> rule7)) -> rule8)) -> rule4) OR ((((((triple8) -> rule3)) -> rule7) ((((triple8) -> rule3) ((((triple8) -> rule3)) -> rule7)) -> rule8)) -> rule4))] Dave is quiet.[(((triple10) -> rule1))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
((((triple3) -> (rule3 % int2))) -> (rule7 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
triple2
((((triple3) -> (rule3 % int2)) triple1) -> (rule8 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
((((triple3) -> (rule3 % int3)) ((((triple3) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is kind.
("Anne" "is" "kind" "+")
triple3
Anne is quiet.
("Anne" "is" "quiet" "+")
triple4
Anne is smart.
("Anne" "is" "smart" "+")
triple5
((triple3) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
((triple1 triple2) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
((triple3 triple4) -> (rule6 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
((triple1 ((((triple3) -> (rule3 % int3)) triple1) -> (rule8 % int2))) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
((((((triple3) -> (rule3 % int3))) -> (rule7 % int2)) triple2) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
((((((triple3) -> (rule3 % int4))) -> (rule7 % int3)) ((((triple3) -> (rule3 % int4)) triple1) -> (rule8 % int2))) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is nice.
("Anne" "is" "nice" "+")
int4
((triple1 ((((triple3) -> (rule3 % int4)) ((((triple3) -> (rule3 % int4))) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is nice.
("Anne" "is" "nice" "+")
int4
((((((triple3) -> (rule3 % int4))) -> (rule7 % int3)) ((((triple3) -> (rule3 % int4)) ((((triple3) -> (rule3 % int4))) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is nice.
("Anne" "is" "nice" "+")
int4
Charlie is cold.
("Charlie" "is" "cold" "+")
triple6
((((triple8) -> (rule3 % int2))) -> (rule7 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
triple7
((((triple8) -> (rule3 % int2)) triple6) -> (rule8 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
((((triple8) -> (rule3 % int3)) ((((triple8) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
triple8
Dave is cold.
("Dave" "is" "cold" "+")
triple9
Dave is young.
("Dave" "is" "young" "+")
triple10
Anne is nice.
("Anne" "is" "nice" "+")
((triple3) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple8) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple8) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
((triple6 triple7) -> (rule4 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
((triple6 ((((triple8) -> (rule3 % int3)) triple6) -> (rule8 % int2))) -> (rule4 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
((((((triple8) -> (rule3 % int3))) -> (rule7 % int2)) triple7) -> (rule4 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
((((((triple8) -> (rule3 % int4))) -> (rule7 % int3)) ((((triple8) -> (rule3 % int4)) triple6) -> (rule8 % int2))) -> (rule4 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
int4
((triple6 ((((triple8) -> (rule3 % int4)) ((((triple8) -> (rule3 % int4))) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
int4
((((((triple8) -> (rule3 % int4))) -> (rule7 % int3)) ((((triple8) -> (rule3 % int4)) ((((triple8) -> (rule3 % int4))) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
int4
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple10) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1