Bob is big. Bob is kind. Bob is red. Harry is big. Harry is green. Harry is round. Harry is smart. If something is round then it is cold. If something is smart then it is big. If something is kind then it is big. All kind, cold things are big. If Bob is red and Bob is round then Bob is big. All red things are round. All smart, cold things are green. If Bob is kind and Bob is green then Bob is cold.
Bob is big.
("Bob" "is" "big" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is red.
("Bob" "is" "red" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If something is round then it is cold.
((("something" "is" "round" "+")) -> ("something" "is" "cold" "+"))
If something is smart then it is big.
((("something" "is" "smart" "+")) -> ("something" "is" "big" "+"))
If something is kind then it is big.
((("something" "is" "kind" "+")) -> ("something" "is" "big" "+"))
All kind, cold things are big.
((("something" "is" "kind" "+") ("something" "is" "cold" "+")) -> ("something" "is" "big" "+"))
If Bob is red and Bob is round then Bob is big.
((("Bob" "is" "red" "+") ("Bob" "is" "round" "+")) -> ("Bob" "is" "big" "+"))
All red things are round.
((("something" "is" "red" "+")) -> ("something" "is" "round" "+"))
All smart, cold things are green.
((("something" "is" "smart" "+") ("something" "is" "cold" "+")) -> ("something" "is" "green" "+"))
If Bob is kind and Bob is green then Bob is cold.
((("Bob" "is" "kind" "+") ("Bob" "is" "green" "+")) -> ("Bob" "is" "cold" "+"))
Harry is green.
True
1
proof
[(triple5 OR ((triple7 ((triple6) -> rule1)) -> rule7))]
("Harry" "is" "green" "+")
triple5
((triple7 ((triple6) -> (rule1 % int2))) -> (rule7 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Bob is not kind.
False
1
inv-proof
[(triple2)]
("Bob" "is" "kind" "-")
triple2
Bob is round.
True
2
proof
[(((triple3) -> rule6))]
("Bob" "is" "round" "+")
((triple3) -> (rule6 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Harry is not cold.
False
2
inv-proof
[(((triple6) -> rule1))]
("Harry" "is" "cold" "-")
((triple6) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Bob is cold.
True
3
proof
[(((((triple3) -> rule6)) -> rule1))]
("Bob" "is" "cold" "+")
((((triple3) -> (rule6 % int2))) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is not cold.
False
3
inv-proof
[(((((triple3) -> rule6)) -> rule1))]
("Bob" "is" "cold" "-")
((((triple3) -> (rule6 % int2))) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is not green.
Unknown
inv-rconc
[@1: Bob is green.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Bob" "is" "green" "-")
Bob is smart.
Unknown
random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "+")
Harry is not kind.
Unknown
inv-random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "-")
Harry is red.
Unknown
random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "+")
@0: Bob is big.[(triple1 OR ((triple2) -> rule3) OR ((triple3 ((triple3) -> rule6)) -> rule5) OR ((triple2 ((((triple3) -> rule6)) -> rule1)) -> rule4))] Bob is kind.[(triple2)] Bob is red.[(triple3)] Harry is big.[(triple4 OR ((triple7) -> rule2))] Harry is green.[(triple5 OR ((triple7 ((triple6) -> rule1)) -> rule7))] Harry is round.[(triple6)] Harry is smart.[(triple7)] @1: Bob is round.[(((triple3) -> rule6))] Harry is cold.[(((triple6) -> rule1))] @2: Bob is cold.[(((((triple3) -> rule6)) -> rule1))]
Bob is big.
("Bob" "is" "big" "+")
triple1
((triple2) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
((triple3 ((triple3) -> (rule6 % int2))) -> (rule5 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
((triple2 ((((triple3) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is kind.
("Bob" "is" "kind" "+")
triple2
Bob is red.
("Bob" "is" "red" "+")
triple3
Harry is big.
("Harry" "is" "big" "+")
triple4
((triple7) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
triple5
((triple7 ((triple6) -> (rule1 % int2))) -> (rule7 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
triple6
Harry is smart.
("Harry" "is" "smart" "+")
triple7
Bob is round.
("Bob" "is" "round" "+")
((triple3) -> (rule6 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
((triple6) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
((((triple3) -> (rule6 % int2))) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2