Bob is big. Bob is cold. Bob is green. Bob is quiet. Bob is red. Bob is rough. Bob is smart. Charlie is big. Charlie is quiet. Charlie is smart. Fiona is cold. Fiona is green. Fiona is quiet. Fiona is red. Fiona is rough. Fiona is smart. All smart, quiet people are green. If Bob is rough and Bob is red then Bob is big. Red, rough people are quiet.
Bob is big.
("Bob" "is" "big" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
All smart, quiet people are green.
((("someone" "is" "smart" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "green" "+"))
If Bob is rough and Bob is red then Bob is big.
((("Bob" "is" "rough" "+") ("Bob" "is" "red" "+")) -> ("Bob" "is" "big" "+"))
Red, rough people are quiet.
((("someone" "is" "red" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "quiet" "+"))
Bob is smart.
True
1
proof
[(triple7)]
("Bob" "is" "smart" "+")
triple7
Charlie is not quiet.
False
1
inv-proof
[(triple9)]
("Charlie" "is" "quiet" "-")
triple9
Charlie is not rough.
Unknown
inv-random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "-")
Fiona is big.
Unknown
random
[@0: Fiona is big.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "big" "+")
@0: Bob is big.[(triple1 OR ((triple6 triple5) -> rule2))] Bob is cold.[(triple2)] Bob is green.[(triple3 OR ((triple7 triple4) -> rule1) OR ((triple7 ((triple5 triple6) -> rule3)) -> rule1))] Bob is quiet.[(triple4 OR ((triple5 triple6) -> rule3))] Bob is red.[(triple5)] Bob is rough.[(triple6)] Bob is smart.[(triple7)] Charlie is big.[(triple8)] Charlie is quiet.[(triple9)] Charlie is smart.[(triple10)] Fiona is cold.[(triple11)] Fiona is green.[(triple12 OR ((triple16 triple13) -> rule1) OR ((triple16 ((triple14 triple15) -> rule3)) -> rule1))] Fiona is quiet.[(triple13 OR ((triple14 triple15) -> rule3))] Fiona is red.[(triple14)] Fiona is rough.[(triple15)] Fiona is smart.[(triple16)] @1: Charlie is green.[(((triple10 triple9) -> rule1))]
Bob is big.
("Bob" "is" "big" "+")
triple1
((triple6 triple5) -> (rule2 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Bob is green.
("Bob" "is" "green" "+")
triple3
((triple7 triple4) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
((triple7 ((triple5 triple6) -> (rule3 % int2))) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
triple4
((triple5 triple6) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
triple5
Bob is rough.
("Bob" "is" "rough" "+")
triple6
Bob is smart.
("Bob" "is" "smart" "+")
triple7
Charlie is big.
("Charlie" "is" "big" "+")
triple8
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple9
Charlie is smart.
("Charlie" "is" "smart" "+")
triple10
Fiona is cold.
("Fiona" "is" "cold" "+")
triple11
Fiona is green.
("Fiona" "is" "green" "+")
triple12
((triple16 triple13) -> (rule1 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
((triple16 ((triple14 triple15) -> (rule3 % int2))) -> (rule1 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple13
((triple14 triple15) -> (rule3 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
triple14
Fiona is rough.
("Fiona" "is" "rough" "+")
triple15
Fiona is smart.
("Fiona" "is" "smart" "+")
triple16
Charlie is green.
("Charlie" "is" "green" "+")
((triple10 triple9) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1