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