Bob is big. Bob is cold. Bob is quiet. Bob is red. Bob is rough. Bob is smart. Bob is young. Erin is big. Erin is quiet. Harry is big. Harry is cold. Harry is red. Harry is rough. Harry is smart. Harry is young. All big, cold things are quiet.
Bob is big.
("Bob" "is" "big" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is young.
("Bob" "is" "young" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is young.
("Harry" "is" "young" "+")
All big, cold things are quiet.
((("something" "is" "big" "+") ("something" "is" "cold" "+")) -> ("something" "is" "quiet" "+"))
Bob is red.
True
1
proof
[(triple4)]
("Bob" "is" "red" "+")
triple4
Harry is not rough.
False
1
inv-proof
[(triple13)]
("Harry" "is" "rough" "-")
triple13
Harry is quiet.
True
3
proof
[(((triple10 triple11) -> rule1))]
("Harry" "is" "quiet" "+")
((triple10 triple11) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is not quiet.
False
3
inv-proof
[(((triple10 triple11) -> rule1))]
("Harry" "is" "quiet" "-")
((triple10 triple11) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Erin is not smart.
Unknown
inv-random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "-")
Erin is rough.
Unknown
random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "+")
Erin is not cold.
Unknown
inv-random
[@0: Erin is cold.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "cold" "-")
Erin is young.
Unknown
random
[@0: Erin is young.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "young" "+")
@0: Bob is big.[(triple1)] Bob is cold.[(triple2)] Bob is quiet.[(triple3 OR ((triple1 triple2) -> rule1))] Bob is red.[(triple4)] Bob is rough.[(triple5)] Bob is smart.[(triple6)] Bob is young.[(triple7)] Erin is big.[(triple8)] Erin is quiet.[(triple9)] Harry is big.[(triple10)] Harry is cold.[(triple11)] Harry is red.[(triple12)] Harry is rough.[(triple13)] Harry is smart.[(triple14)] Harry is young.[(triple15)] @1: Harry is quiet.[(((triple10 triple11) -> rule1))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Bob is quiet.
("Bob" "is" "quiet" "+")
triple3
((triple1 triple2) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
triple4
Bob is rough.
("Bob" "is" "rough" "+")
triple5
Bob is smart.
("Bob" "is" "smart" "+")
triple6
Bob is young.
("Bob" "is" "young" "+")
triple7
Erin is big.
("Erin" "is" "big" "+")
triple8
Erin is quiet.
("Erin" "is" "quiet" "+")
triple9
Harry is big.
("Harry" "is" "big" "+")
triple10
Harry is cold.
("Harry" "is" "cold" "+")
triple11
Harry is red.
("Harry" "is" "red" "+")
triple12
Harry is rough.
("Harry" "is" "rough" "+")
triple13
Harry is smart.
("Harry" "is" "smart" "+")
triple14
Harry is young.
("Harry" "is" "young" "+")
triple15
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple10 triple11) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1