Bob is big. Bob is blue. Bob is cold. Bob is kind. Bob is quiet. Erin is quiet. Gary is green. Gary is round. Harry is big. Harry is blue. If Erin is kind then Erin is blue. Quiet people are kind. If someone is big and kind then they are cold. Big, round people are quiet. All round people are green. If someone is big then they are kind. Cold, blue people are big. Round, cold people are big.
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is round.
("Gary" "is" "round" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is blue.
("Harry" "is" "blue" "+")
If Erin is kind then Erin is blue.
((("Erin" "is" "kind" "+")) -> ("Erin" "is" "blue" "+"))
Quiet people are kind.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "kind" "+"))
If someone is big and kind then they are cold.
((("someone" "is" "big" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "cold" "+"))
Big, round people are quiet.
((("someone" "is" "big" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "quiet" "+"))
All round people are green.
((("someone" "is" "round" "+")) -> ("someone" "is" "green" "+"))
If someone is big then they are kind.
((("someone" "is" "big" "+")) -> ("someone" "is" "kind" "+"))
Cold, blue people are big.
((("someone" "is" "cold" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "big" "+"))
Round, cold people are big.
((("someone" "is" "round" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "big" "+"))
Bob is cold.
True
1
proof
[(triple3 OR ((triple1 triple4) -> rule3) OR ((triple1 ((triple1) -> rule6)) -> rule3) OR ((triple1 ((triple5) -> rule2)) -> rule3))]
("Bob" "is" "cold" "+")
triple3
((triple1 triple4) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
((triple1 ((triple1) -> (rule6 % int2))) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
((triple1 ((triple5) -> (rule2 % int2))) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Gary is not round.
False
1
inv-proof
[(triple8)]
("Gary" "is" "round" "-")
triple8
Harry is kind.
True
2
proof
[(((triple9) -> rule6))]
("Harry" "is" "kind" "+")
((triple9) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Erin is not kind.
False
2
inv-proof
[(((triple6) -> rule2))]
("Erin" "is" "kind" "-")
((triple6) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Harry is cold.
True
4
proof
[(((triple9 ((triple9) -> rule6)) -> rule3))]
("Harry" "is" "cold" "+")
((triple9 ((triple9) -> (rule6 % int2))) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Erin is not blue.
False
3
inv-proof
[(((((triple6) -> rule2)) -> rule1))]
("Erin" "is" "blue" "-")
((((triple6) -> (rule2 % int2))) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Harry is not quiet.
Unknown
inv-rconc
[@1: Harry is quiet.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Harry" "is" "quiet" "-")
Gary is cold.
Unknown
rconc
[@2: Gary is cold.[CWA. Example of deepest failure = (rule3 <- rule7 <- FAIL)]]
("Gary" "is" "cold" "+")
Gary is not big.
Unknown
inv-rconc
[@3: Gary is big.[CWA. Example of deepest failure = (rule8 <- rule3 <- rule7 <- FAIL)]]
("Gary" "is" "big" "-")
Gary is blue.
Unknown
random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "+")
Bob is not round.
Unknown
inv-random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "-")
Erin is round.
Unknown
random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "+")
@0: Bob is big.[(triple1 OR ((triple3 triple2) -> rule7))] Bob is blue.[(triple2)] Bob is cold.[(triple3 OR ((triple1 triple4) -> rule3) OR ((triple1 ((triple1) -> rule6)) -> rule3) OR ((triple1 ((triple5) -> rule2)) -> rule3))] Bob is kind.[(triple4 OR ((triple1) -> rule6) OR ((triple5) -> rule2) OR ((((triple3 triple2) -> rule7)) -> rule6))] Bob is quiet.[(triple5)] Erin is quiet.[(triple6)] Gary is green.[(triple7 OR ((triple8) -> rule5))] Gary is round.[(triple8)] Harry is big.[(triple9)] Harry is blue.[(triple10)] @1: Erin is kind.[(((triple6) -> rule2))] Harry is kind.[(((triple9) -> rule6))] @2: Erin is blue.[(((((triple6) -> rule2)) -> rule1))] Harry is cold.[(((triple9 ((triple9) -> rule6)) -> rule3))]
Bob is big.
("Bob" "is" "big" "+")
triple1
((triple3 triple2) -> (rule7 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
triple2
Bob is cold.
("Bob" "is" "cold" "+")
triple3
((triple1 triple4) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
((triple1 ((triple1) -> (rule6 % int2))) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
((triple1 ((triple5) -> (rule2 % int2))) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
triple4
((triple1) -> (rule6 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((triple5) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((((triple3 triple2) -> (rule7 % int2))) -> (rule6 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
triple5
Erin is quiet.
("Erin" "is" "quiet" "+")
triple6
Gary is green.
("Gary" "is" "green" "+")
triple7
((triple8) -> (rule5 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
triple8
Harry is big.
("Harry" "is" "big" "+")
triple9
Harry is blue.
("Harry" "is" "blue" "+")
triple10
Erin is kind.
("Erin" "is" "kind" "+")
((triple6) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
((triple9) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
((((triple6) -> (rule2 % int2))) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
((triple9 ((triple9) -> (rule6 % int2))) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2