Bob is nice. Bob is white. Charlie is big. Charlie is cold. Charlie is kind. Charlie is nice. Charlie is red. Charlie is white. Dave is furry. Dave is nice. Dave is red. Dave is white. Fiona is cold. Fiona is kind. Fiona is nice. If Bob is red then Bob is big. If something is white then it is big. Kind, nice things are big. All nice, kind things are furry. Furry, big things are kind. If Charlie is big and Charlie is kind then Charlie is cold. If Fiona is white and Fiona is cold then Fiona is kind. Big, kind things are nice.
Bob is nice.
("Bob" "is" "nice" "+")
Bob is white.
("Bob" "is" "white" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is white.
("Dave" "is" "white" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
If Bob is red then Bob is big.
((("Bob" "is" "red" "+")) -> ("Bob" "is" "big" "+"))
If something is white then it is big.
((("something" "is" "white" "+")) -> ("something" "is" "big" "+"))
Kind, nice things are big.
((("something" "is" "kind" "+") ("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
All nice, kind things are furry.
((("something" "is" "nice" "+") ("something" "is" "kind" "+")) -> ("something" "is" "furry" "+"))
Furry, big things are kind.
((("something" "is" "furry" "+") ("something" "is" "big" "+")) -> ("something" "is" "kind" "+"))
If Charlie is big and Charlie is kind then Charlie is cold.
((("Charlie" "is" "big" "+") ("Charlie" "is" "kind" "+")) -> ("Charlie" "is" "cold" "+"))
If Fiona is white and Fiona is cold then Fiona is kind.
((("Fiona" "is" "white" "+") ("Fiona" "is" "cold" "+")) -> ("Fiona" "is" "kind" "+"))
Big, kind things are nice.
((("something" "is" "big" "+") ("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
Bob is white.
True
1
proof
[(triple2)]
("Bob" "is" "white" "+")
triple2
Charlie is not cold.
False
1
inv-proof
[(triple4 OR ((triple3 triple5) -> rule6) OR ((((triple8) -> rule2) triple5) -> rule6) OR ((((triple5 triple6) -> rule3) triple5) -> rule6))]
("Charlie" "is" "cold" "-")
triple4
((triple3 triple5) -> (rule6 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
((((triple8) -> (rule2 % int2)) triple5) -> (rule6 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
((((triple5 triple6) -> (rule3 % int2)) triple5) -> (rule6 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Fiona is big.
True
3
proof
[(((triple14 triple15) -> rule3))]
("Fiona" "is" "big" "+")
((triple14 triple15) -> (rule3 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is not furry.
False
3
inv-proof
[(((triple15 triple14) -> rule4))]
("Fiona" "is" "furry" "-")
((triple15 triple14) -> (rule4 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Bob is not furry.
Unknown
inv-rconc
[@2: Bob is furry.[CWA. Example of deepest failure = (rule4 <- rule5 <- FAIL)]]
("Bob" "is" "furry" "-")
Bob is kind.
Unknown
rconc
[@2: Bob is kind.[CWA. Example of deepest failure = (rule5 <- rule4 <- FAIL)]]
("Bob" "is" "kind" "+")
Fiona is not white.
Unknown
inv-random
[@0: Fiona is white.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "white" "-")
Dave is cold.
Unknown
random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "+")
@0: Bob is nice.[(triple1)] Bob is white.[(triple2)] Charlie is big.[(triple3 OR ((triple8) -> rule2) OR ((triple5 triple6) -> rule3))] Charlie is cold.[(triple4 OR ((triple3 triple5) -> rule6) OR ((((triple8) -> rule2) triple5) -> rule6) OR ((((triple5 triple6) -> rule3) triple5) -> rule6))] Charlie is kind.[(triple5)] Charlie is nice.[(triple6 OR ((triple3 triple5) -> rule8) OR ((((triple8) -> rule2) triple5) -> rule8))] Charlie is red.[(triple7)] Charlie is white.[(triple8)] Dave is furry.[(triple9)] Dave is nice.[(triple10 OR ((((triple12) -> rule2) ((triple9 ((triple12) -> rule2)) -> rule5)) -> rule8))] Dave is red.[(triple11)] Dave is white.[(triple12)] Fiona is cold.[(triple13)] Fiona is kind.[(triple14)] Fiona is nice.[(triple15)] @1: Bob is big.[(((triple2) -> rule2))] Charlie is furry.[(((triple6 triple5) -> rule4) OR ((((triple3 triple5) -> rule8) triple5) -> rule4) OR ((((((triple8) -> rule2) triple5) -> rule8) triple5) -> rule4))] Dave is big.[(((triple12) -> rule2))] Fiona is big.[(((triple14 triple15) -> rule3))] Fiona is furry.[(((triple15 triple14) -> rule4))] @2: Dave is kind.[(((triple9 ((triple12) -> rule2)) -> rule5))]
Bob is nice.
("Bob" "is" "nice" "+")
triple1
Bob is white.
("Bob" "is" "white" "+")
triple2
Charlie is big.
("Charlie" "is" "big" "+")
triple3
((triple8) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((triple5 triple6) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple4
((triple3 triple5) -> (rule6 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
((((triple8) -> (rule2 % int2)) triple5) -> (rule6 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
((((triple5 triple6) -> (rule3 % int2)) triple5) -> (rule6 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
triple5
Charlie is nice.
("Charlie" "is" "nice" "+")
triple6
((triple3 triple5) -> (rule8 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
((((triple8) -> (rule2 % int2)) triple5) -> (rule8 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
triple7
Charlie is white.
("Charlie" "is" "white" "+")
triple8
Dave is furry.
("Dave" "is" "furry" "+")
triple9
Dave is nice.
("Dave" "is" "nice" "+")
triple10
((((triple12) -> (rule2 % int3)) ((triple9 ((triple12) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is red.
("Dave" "is" "red" "+")
triple11
Dave is white.
("Dave" "is" "white" "+")
triple12
Fiona is cold.
("Fiona" "is" "cold" "+")
triple13
Fiona is kind.
("Fiona" "is" "kind" "+")
triple14
Fiona is nice.
("Fiona" "is" "nice" "+")
triple15
Bob is big.
("Bob" "is" "big" "+")
((triple2) -> (rule2 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple6 triple5) -> (rule4 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
((((triple3 triple5) -> (rule8 % int2)) triple5) -> (rule4 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
((((((triple8) -> (rule2 % int3)) triple5) -> (rule8 % int2)) triple5) -> (rule4 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Dave is big.
("Dave" "is" "big" "+")
((triple12) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
((triple14 triple15) -> (rule3 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
((triple15 triple14) -> (rule4 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
((triple9 ((triple12) -> (rule2 % int2))) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2