Bob is blue. Bob is not green. Bob is smart. Charlie is green. Charlie is rough. Erin is blue. Erin is green. Erin is nice. Erin is rough. Erin is smart. Furry people are rough. Rough people are furry. All blue, smart people are furry. If someone is rough and not nice then they are green. If someone is green and not smart then they are young. Rough people are young. If Bob is rough and Bob is green then Bob is not blue. If Erin is nice then Erin is young.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is not green.
("Bob" "is" "green" "-")
Bob is smart.
("Bob" "is" "smart" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Furry people are rough.
((("someone" "is" "furry" "+")) -> ("someone" "is" "rough" "+"))
Rough people are furry.
((("someone" "is" "rough" "+")) -> ("someone" "is" "furry" "+"))
All blue, smart people are furry.
((("someone" "is" "blue" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "furry" "+"))
If someone is rough and not nice then they are green.
((("someone" "is" "rough" "+") ("someone" "is" "nice" "~")) -> ("someone" "is" "green" "+"))
If someone is green and not smart then they are young.
((("someone" "is" "green" "+") ("someone" "is" "smart" "~")) -> ("someone" "is" "young" "+"))
Rough people are young.
((("someone" "is" "rough" "+")) -> ("someone" "is" "young" "+"))
If Bob is rough and Bob is green then Bob is not blue.
((("Bob" "is" "rough" "+") ("Bob" "is" "green" "+")) -> ("Bob" "is" "blue" "-"))
If Erin is nice then Erin is young.
((("Erin" "is" "nice" "+")) -> ("Erin" "is" "young" "+"))
Erin is blue.
True
1
proof
[(triple6)]
("Erin" "is" "blue" "+")
triple6
Erin is not nice.
False
1
inv-proof
[(triple8)]
("Erin" "is" "nice" "-")
triple8
Charlie is furry.
True
2
proof
[(((triple5) -> rule2))]
("Charlie" "is" "furry" "+")
((triple5) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Bob is not furry.
False
3
inv-proof
[(((triple1 triple3) -> rule3))]
("Bob" "is" "furry" "-")
((triple1 triple3) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is rough.
True
4
proof
[(((((triple1 triple3) -> rule3)) -> rule1))]
("Bob" "is" "rough" "+")
((((triple1 triple3) -> (rule3 % int2))) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is not rough.
False
4
inv-proof
[(((((triple1 triple3) -> rule3)) -> rule1))]
("Bob" "is" "rough" "-")
((((triple1 triple3) -> (rule3 % int2))) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is young.
True
5
proof
[(((((((triple1 triple3) -> rule3)) -> rule1)) -> rule6))]
("Bob" "is" "young" "+")
((((((triple1 triple3) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is not young.
False
5
inv-proof
[(((((((triple1 triple3) -> rule3)) -> rule1)) -> rule6))]
("Bob" "is" "young" "-")
((((((triple1 triple3) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Charlie is not nice.
Unknown
inv-random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "-")
Charlie is blue.
Unknown
random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "+")
Charlie is not smart.
Unknown
inv-random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "-")
Bob is nice.
Unknown
random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "+")
@0: Bob is blue.[(triple1)] Bob is not green.[(triple2)] Bob is smart.[(triple3)] Charlie is green.[(triple4)] Charlie is rough.[(triple5)] Erin is blue.[(triple6)] Erin is green.[(triple7)] Erin is nice.[(triple8)] Erin is rough.[(triple9 OR ((((triple6 triple10) -> rule3)) -> rule1))] Erin is smart.[(triple10)] @1: Bob is furry.[(((triple1 triple3) -> rule3))] Charlie is furry.[(((triple5) -> rule2))] Charlie is young.[(((triple5) -> rule6))] Erin is furry.[(((triple9) -> rule2) OR ((triple6 triple10) -> rule3))] Erin is young.[(((triple8) -> rule8) OR ((triple9) -> rule6) OR ((((((triple6 triple10) -> rule3)) -> rule1)) -> rule6))] @2: Bob is rough.[(((((triple1 triple3) -> rule3)) -> rule1))] @3: Bob is young.[(((((((triple1 triple3) -> rule3)) -> rule1)) -> rule6))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is not green.
("Bob" "is" "green" "-")
triple2
Bob is smart.
("Bob" "is" "smart" "+")
triple3
Charlie is green.
("Charlie" "is" "green" "+")
triple4
Charlie is rough.
("Charlie" "is" "rough" "+")
triple5
Erin is blue.
("Erin" "is" "blue" "+")
triple6
Erin is green.
("Erin" "is" "green" "+")
triple7
Erin is nice.
("Erin" "is" "nice" "+")
triple8
Erin is rough.
("Erin" "is" "rough" "+")
triple9
((((triple6 triple10) -> (rule3 % int2))) -> (rule1 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
triple10
Bob is furry.
("Bob" "is" "furry" "+")
((triple1 triple3) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple5) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
((triple5) -> (rule6 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
((triple9) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
((triple6 triple10) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
((triple8) -> (rule8 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
((triple9) -> (rule6 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
((((((triple6 triple10) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Bob is rough.
("Bob" "is" "rough" "+")
((((triple1 triple3) -> (rule3 % int2))) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
((((((triple1 triple3) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3