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