Bob is blue. Bob is young. Dave is blue. Dave is green. Dave is kind. Dave is not nice. Erin is kind. Erin is nice. Erin is rough. Erin is young. Blue things are young. If something is rough and kind then it is green. If something is blue and not kind then it is green. If Erin is kind and Erin is nice then Erin is quiet. If something is young then it is quiet. All rough things are nice.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is young.
("Bob" "is" "young" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is not nice.
("Dave" "is" "nice" "-")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is young.
("Erin" "is" "young" "+")
Blue things are young.
((("something" "is" "blue" "+")) -> ("something" "is" "young" "+"))
If something is rough and kind then it is green.
((("something" "is" "rough" "+") ("something" "is" "kind" "+")) -> ("something" "is" "green" "+"))
If something is blue and not kind then it is green.
((("something" "is" "blue" "+") ("something" "is" "kind" "~")) -> ("something" "is" "green" "+"))
If Erin is kind and Erin is nice then Erin is quiet.
((("Erin" "is" "kind" "+") ("Erin" "is" "nice" "+")) -> ("Erin" "is" "quiet" "+"))
If something is young then it is quiet.
((("something" "is" "young" "+")) -> ("something" "is" "quiet" "+"))
All rough things are nice.
((("something" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
Dave is kind.
True
1
proof
[(triple5)]
("Dave" "is" "kind" "+")
triple5
Erin is not nice.
False
1
inv-proof
[(triple8 OR ((triple9) -> rule6))]
("Erin" "is" "nice" "-")
triple8
((triple9) -> (rule6 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is quiet.
True
2
proof
[(((triple10) -> rule5) OR ((triple7 triple8) -> rule4) OR ((triple7 ((triple9) -> rule6)) -> rule4))]
("Erin" "is" "quiet" "+")
((triple10) -> (rule5 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((triple7 triple8) -> (rule4 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((triple7 ((triple9) -> (rule6 % int2))) -> (rule4 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Dave is not young.
False
2
inv-proof
[(((triple3) -> rule1))]
("Dave" "is" "young" "-")
((triple3) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is quiet.
True
3
proof
[(((((triple3) -> rule1)) -> rule5))]
("Dave" "is" "quiet" "+")
((((triple3) -> (rule1 % int2))) -> (rule5 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is not quiet.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule5))]
("Dave" "is" "quiet" "-")
((((triple3) -> (rule1 % int2))) -> (rule5 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Bob is not green.
Unknown
inv-rconc
[@1: Bob is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "green" "-")
Bob is nice.
Unknown
rconc
[@1: Bob is nice.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "nice" "+")
Erin is not blue.
Unknown
inv-random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "-")
Dave is rough.
Unknown
random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "+")
Bob is not kind.
Unknown
inv-random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "-")
Bob is rough.
Unknown
random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "+")
@0: Bob is blue.[(triple1)] Bob is young.[(triple2 OR ((triple1) -> rule1))] Dave is blue.[(triple3)] Dave is green.[(triple4)] Dave is kind.[(triple5)] Dave is not nice.[(triple6)] Erin is kind.[(triple7)] Erin is nice.[(triple8 OR ((triple9) -> rule6))] Erin is rough.[(triple9)] Erin is young.[(triple10)] @1: Bob is quiet.[(((triple2) -> rule5) OR ((((triple1) -> rule1)) -> rule5))] Dave is young.[(((triple3) -> rule1))] Erin is green.[(((triple9 triple7) -> rule2))] Erin is quiet.[(((triple10) -> rule5) OR ((triple7 triple8) -> rule4) OR ((triple7 ((triple9) -> rule6)) -> rule4))] @2: Dave is quiet.[(((((triple3) -> rule1)) -> rule5))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is young.
("Bob" "is" "young" "+")
triple2
((triple1) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
triple3
Dave is green.
("Dave" "is" "green" "+")
triple4
Dave is kind.
("Dave" "is" "kind" "+")
triple5
Dave is not nice.
("Dave" "is" "nice" "-")
triple6
Erin is kind.
("Erin" "is" "kind" "+")
triple7
Erin is nice.
("Erin" "is" "nice" "+")
triple8
((triple9) -> (rule6 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
triple9
Erin is young.
("Erin" "is" "young" "+")
triple10
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple2) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
((triple3) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
((triple9 triple7) -> (rule2 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
((triple10) -> (rule5 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((triple7 triple8) -> (rule4 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((triple7 ((triple9) -> (rule6 % int2))) -> (rule4 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
((((triple3) -> (rule1 % int2))) -> (rule5 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2