Bob is big. Bob is kind. Bob is smart. Erin is big. Erin is kind. Erin is red. Erin is rough. Erin is smart. Erin is white. Gary is big. Gary is kind. Gary is rough. Gary is smart. Harry is big. Harry is kind. Harry is smart. If someone is rough then they are big.
Bob is big.
("Bob" "is" "big" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is white.
("Erin" "is" "white" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If someone is rough then they are big.
((("someone" "is" "rough" "+")) -> ("someone" "is" "big" "+"))
Gary is rough.
True
1
proof
[(triple12)]
("Gary" "is" "rough" "+")
triple12
Gary is not rough.
False
1
inv-proof
[(triple12)]
("Gary" "is" "rough" "-")
triple12
Gary is not white.
Unknown
inv-random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "-")
Harry is white.
Unknown
random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "+")
@0: Bob is big.[(triple1)] Bob is kind.[(triple2)] Bob is smart.[(triple3)] Erin is big.[(triple4 OR ((triple7) -> rule1))] Erin is kind.[(triple5)] Erin is red.[(triple6)] Erin is rough.[(triple7)] Erin is smart.[(triple8)] Erin is white.[(triple9)] Gary is big.[(triple10 OR ((triple12) -> rule1))] Gary is kind.[(triple11)] Gary is rough.[(triple12)] Gary is smart.[(triple13)] Harry is big.[(triple14)] Harry is kind.[(triple15)] Harry is smart.[(triple16)]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is kind.
("Bob" "is" "kind" "+")
triple2
Bob is smart.
("Bob" "is" "smart" "+")
triple3
Erin is big.
("Erin" "is" "big" "+")
triple4
((triple7) -> (rule1 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
triple5
Erin is red.
("Erin" "is" "red" "+")
triple6
Erin is rough.
("Erin" "is" "rough" "+")
triple7
Erin is smart.
("Erin" "is" "smart" "+")
triple8
Erin is white.
("Erin" "is" "white" "+")
triple9
Gary is big.
("Gary" "is" "big" "+")
triple10
((triple12) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
triple11
Gary is rough.
("Gary" "is" "rough" "+")
triple12
Gary is smart.
("Gary" "is" "smart" "+")
triple13
Harry is big.
("Harry" "is" "big" "+")
triple14
Harry is kind.
("Harry" "is" "kind" "+")
triple15
Harry is smart.
("Harry" "is" "smart" "+")
triple16