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