Bob is cold. Bob is smart. Bob is young. Charlie is nice. Charlie is quiet. Charlie is rough. Dave is quiet. Smart things are quiet. If something is furry and rough then it is quiet. If something is quiet then it is nice. If Dave is rough then Dave is smart. If something is young then it is rough. If Dave is quiet then Dave is young. If something is quiet and furry then it is nice. If something is rough then it is cold.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is young.
("Bob" "is" "young" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Smart things are quiet.
((("something" "is" "smart" "+")) -> ("something" "is" "quiet" "+"))
If something is furry and rough then it is quiet.
((("something" "is" "furry" "+") ("something" "is" "rough" "+")) -> ("something" "is" "quiet" "+"))
If something is quiet then it is nice.
((("something" "is" "quiet" "+")) -> ("something" "is" "nice" "+"))
If Dave is rough then Dave is smart.
((("Dave" "is" "rough" "+")) -> ("Dave" "is" "smart" "+"))
If something is young then it is rough.
((("something" "is" "young" "+")) -> ("something" "is" "rough" "+"))
If Dave is quiet then Dave is young.
((("Dave" "is" "quiet" "+")) -> ("Dave" "is" "young" "+"))
If something is quiet and furry then it is nice.
((("something" "is" "quiet" "+") ("something" "is" "furry" "+")) -> ("something" "is" "nice" "+"))
If something is rough then it is cold.
((("something" "is" "rough" "+")) -> ("something" "is" "cold" "+"))
Dave is quiet.
True
1
proof
[(triple7)]
("Dave" "is" "quiet" "+")
triple7
Dave is not quiet.
False
1
inv-proof
[(triple7)]
("Dave" "is" "quiet" "-")
triple7
Bob is quiet.
True
2
proof
[(((triple2) -> rule1))]
("Bob" "is" "quiet" "+")
((triple2) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Dave is not young.
False
2
inv-proof
[(((triple7) -> rule6))]
("Dave" "is" "young" "-")
((triple7) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Bob is nice.
True
3
proof
[(((((triple2) -> rule1)) -> rule3))]
("Bob" "is" "nice" "+")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Dave is not rough.
False
3
inv-proof
[(((((triple7) -> rule6)) -> rule5))]
("Dave" "is" "rough" "-")
((((triple7) -> (rule6 % int2))) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is cold.
True
4
proof
[(((((((triple7) -> rule6)) -> rule5)) -> rule8))]
("Dave" "is" "cold" "+")
((((((triple7) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is not cold.
False
4
inv-proof
[(((((((triple7) -> rule6)) -> rule5)) -> rule8))]
("Dave" "is" "cold" "-")
((((((triple7) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Charlie is not young.
Unknown
inv-random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "-")
Charlie is smart.
Unknown
random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "+")
Dave is not furry.
Unknown
inv-random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "-")
Charlie is furry.
Unknown
random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "+")
@0: Bob is cold.[(triple1 OR ((((triple3) -> rule5)) -> rule8))] Bob is smart.[(triple2)] Bob is young.[(triple3)] Charlie is nice.[(triple4 OR ((triple5) -> rule3))] Charlie is quiet.[(triple5)] Charlie is rough.[(triple6)] Dave is quiet.[(triple7)] @1: Bob is quiet.[(((triple2) -> rule1))] Bob is rough.[(((triple3) -> rule5))] Charlie is cold.[(((triple6) -> rule8))] Dave is nice.[(((triple7) -> rule3))] Dave is young.[(((triple7) -> rule6))] @2: Bob is nice.[(((((triple2) -> rule1)) -> rule3))] Dave is rough.[(((((triple7) -> rule6)) -> rule5))] @3: Dave is cold.[(((((((triple7) -> rule6)) -> rule5)) -> rule8))] Dave is smart.[(((((((triple7) -> rule6)) -> rule5)) -> rule4))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
((((triple3) -> (rule5 % int2))) -> (rule8 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
triple2
Bob is young.
("Bob" "is" "young" "+")
triple3
Charlie is nice.
("Charlie" "is" "nice" "+")
triple4
((triple5) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple5
Charlie is rough.
("Charlie" "is" "rough" "+")
triple6
Dave is quiet.
("Dave" "is" "quiet" "+")
triple7
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple2) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
((triple3) -> (rule5 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple6) -> (rule8 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
((triple7) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
((triple7) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
((((triple7) -> (rule6 % int2))) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
((((((triple7) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
((((((triple7) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3