Bob is cold. Bob is green. Dave is big. Dave is cold. Dave is green. Dave is nice. Dave is quiet. Erin is big. Erin is kind. Erin is nice. All quiet, kind things are green. If something is big and nice then it is quiet. All big, green things are cold. If Erin is furry and Erin is kind then Erin is cold. If something is cold then it is green. If something is cold and kind then it is quiet. Nice, kind things are big. Cold, kind things are nice.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is green.
("Bob" "is" "green" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is nice.
("Erin" "is" "nice" "+")
All quiet, kind things are green.
((("something" "is" "quiet" "+") ("something" "is" "kind" "+")) -> ("something" "is" "green" "+"))
If something is big and nice then it is quiet.
((("something" "is" "big" "+") ("something" "is" "nice" "+")) -> ("something" "is" "quiet" "+"))
All big, green things are cold.
((("something" "is" "big" "+") ("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
If Erin is furry and Erin is kind then Erin is cold.
((("Erin" "is" "furry" "+") ("Erin" "is" "kind" "+")) -> ("Erin" "is" "cold" "+"))
If something is cold then it is green.
((("something" "is" "cold" "+")) -> ("something" "is" "green" "+"))
If something is cold and kind then it is quiet.
((("something" "is" "cold" "+") ("something" "is" "kind" "+")) -> ("something" "is" "quiet" "+"))
Nice, kind things are big.
((("something" "is" "nice" "+") ("something" "is" "kind" "+")) -> ("something" "is" "big" "+"))
Cold, kind things are nice.
((("something" "is" "cold" "+") ("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
Dave is cold.
True
1
proof
[(triple4 OR ((triple3 triple5) -> rule3))]
("Dave" "is" "cold" "+")
triple4
((triple3 triple5) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Bob is not cold.
False
1
inv-proof
[(triple1)]
("Bob" "is" "cold" "-")
triple1
Erin is quiet.
True
3
proof
[(((triple8 triple10) -> rule2) OR ((((triple10 triple9) -> rule7) triple10) -> rule2))]
("Erin" "is" "quiet" "+")
((triple8 triple10) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((((triple10 triple9) -> (rule7 % int2)) triple10) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is not quiet.
False
3
inv-proof
[(((triple8 triple10) -> rule2) OR ((((triple10 triple9) -> rule7) triple10) -> rule2))]
("Erin" "is" "quiet" "-")
((triple8 triple10) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((((triple10 triple9) -> (rule7 % int2)) triple10) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is green.
True
5
proof
[(((((triple8 triple10) -> rule2) triple9) -> rule1) OR ((((((triple10 triple9) -> rule7) triple10) -> rule2) triple9) -> rule1))]
("Erin" "is" "green" "+")
((((triple8 triple10) -> (rule2 % int2)) triple9) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
((((((triple10 triple9) -> (rule7 % int3)) triple10) -> (rule2 % int2)) triple9) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is not green.
False
5
inv-proof
[(((((triple8 triple10) -> rule2) triple9) -> rule1) OR ((((((triple10 triple9) -> rule7) triple10) -> rule2) triple9) -> rule1))]
("Erin" "is" "green" "-")
((((triple8 triple10) -> (rule2 % int2)) triple9) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
((((((triple10 triple9) -> (rule7 % int3)) triple10) -> (rule2 % int2)) triple9) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Bob is not quiet.
Unknown
inv-rconc
[@2: Bob is quiet.[CWA. Example of deepest failure = (rule2 <- rule7 <- FAIL)]]
("Bob" "is" "quiet" "-")
Bob is big.
Unknown
rconc
[@1: Bob is big.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Bob" "is" "big" "+")
Bob is not nice.
Unknown
inv-rconc
[@1: Bob is nice.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Bob" "is" "nice" "-")
Dave is kind.
Unknown
random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "+")
Erin is not furry.
Unknown
inv-random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "-")
Bob is furry.
Unknown
random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "+")
@0: Bob is cold.[(triple1)] Bob is green.[(triple2 OR ((triple1) -> rule5))] Dave is big.[(triple3)] Dave is cold.[(triple4 OR ((triple3 triple5) -> rule3))] Dave is green.[(triple5 OR ((triple4) -> rule5))] Dave is nice.[(triple6)] Dave is quiet.[(triple7 OR ((triple3 triple6) -> rule2))] Erin is big.[(triple8 OR ((triple10 triple9) -> rule7))] Erin is kind.[(triple9)] Erin is nice.[(triple10)] @1: Erin is quiet.[(((triple8 triple10) -> rule2) OR ((((triple10 triple9) -> rule7) triple10) -> rule2))] @2: Erin is green.[(((((triple8 triple10) -> rule2) triple9) -> rule1) OR ((((((triple10 triple9) -> rule7) triple10) -> rule2) triple9) -> rule1))] @3: Erin is cold.[(((triple8 ((((triple8 triple10) -> rule2) triple9) -> rule1)) -> rule3) OR ((((triple10 triple9) -> rule7) ((((triple8 triple10) -> rule2) triple9) -> rule1)) -> rule3) OR ((triple8 ((((((triple10 triple9) -> rule7) triple10) -> rule2) triple9) -> rule1)) -> rule3) OR ((((triple10 triple9) -> rule7) ((((((triple10 triple9) -> rule7) triple10) -> rule2) triple9) -> rule1)) -> rule3))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
triple2
((triple1) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
triple3
Dave is cold.
("Dave" "is" "cold" "+")
triple4
((triple3 triple5) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
triple5
((triple4) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
triple6
Dave is quiet.
("Dave" "is" "quiet" "+")
triple7
((triple3 triple6) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
triple8
((triple10 triple9) -> (rule7 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
triple9
Erin is nice.
("Erin" "is" "nice" "+")
triple10
Erin is quiet.
("Erin" "is" "quiet" "+")
((triple8 triple10) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((((triple10 triple9) -> (rule7 % int2)) triple10) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
((((triple8 triple10) -> (rule2 % int2)) triple9) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
((((((triple10 triple9) -> (rule7 % int3)) triple10) -> (rule2 % int2)) triple9) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is cold.
("Erin" "is" "cold" "+")
((triple8 ((((triple8 triple10) -> (rule2 % int3)) triple9) -> (rule1 % int2))) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
((((triple10 triple9) -> (rule7 % int4)) ((((triple8 triple10) -> (rule2 % int3)) triple9) -> (rule1 % int2))) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Erin is big.
("Erin" "is" "big" "+")
int4
((triple8 ((((((triple10 triple9) -> (rule7 % int4)) triple10) -> (rule2 % int3)) triple9) -> (rule1 % int2))) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Erin is big.
("Erin" "is" "big" "+")
int4
((((triple10 triple9) -> (rule7 % int4)) ((((((triple10 triple9) -> (rule7 % int4)) triple10) -> (rule2 % int3)) triple9) -> (rule1 % int2))) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Erin is big.
("Erin" "is" "big" "+")
int4