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