Bob is cold. Bob is green. Bob is quiet. Bob is red. Bob is round. Bob is white. Bob is young. Harry is red. Harry is round. Harry is white. If something is quiet then it is young. Red things are quiet.
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 round.
("Bob" "is" "round" "+")
Bob is white.
("Bob" "is" "white" "+")
Bob is young.
("Bob" "is" "young" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is white.
("Harry" "is" "white" "+")
If something is quiet then it is young.
((("something" "is" "quiet" "+")) -> ("something" "is" "young" "+"))
Red things are quiet.
((("something" "is" "red" "+")) -> ("something" "is" "quiet" "+"))
Bob is red.
True
1
proof
[(triple4)]
("Bob" "is" "red" "+")
triple4
Harry is not red.
False
1
inv-proof
[(triple8)]
("Harry" "is" "red" "-")
triple8
Harry is quiet.
True
2
proof
[(((triple8) -> rule2))]
("Harry" "is" "quiet" "+")
((triple8) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is not quiet.
False
2
inv-proof
[(((triple8) -> rule2))]
("Harry" "is" "quiet" "-")
((triple8) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is young.
True
3
proof
[(((((triple8) -> rule2)) -> rule1))]
("Harry" "is" "young" "+")
((((triple8) -> (rule2 % int2))) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is not young.
False
3
inv-proof
[(((((triple8) -> rule2)) -> rule1))]
("Harry" "is" "young" "-")
((((triple8) -> (rule2 % int2))) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is not green.
Unknown
inv-random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "-")
Harry is cold.
Unknown
random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "+")
@0: Bob is cold.[(triple1)] Bob is green.[(triple2)] Bob is quiet.[(triple3 OR ((triple4) -> rule2))] Bob is red.[(triple4)] Bob is round.[(triple5)] Bob is white.[(triple6)] Bob is young.[(triple7 OR ((triple3) -> rule1) OR ((((triple4) -> rule2)) -> rule1))] Harry is red.[(triple8)] Harry is round.[(triple9)] Harry is white.[(triple10)] @1: Harry is quiet.[(((triple8) -> rule2))] @2: Harry is young.[(((((triple8) -> rule2)) -> rule1))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
triple2
Bob is quiet.
("Bob" "is" "quiet" "+")
triple3
((triple4) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
triple4
Bob is round.
("Bob" "is" "round" "+")
triple5
Bob is white.
("Bob" "is" "white" "+")
triple6
Bob is young.
("Bob" "is" "young" "+")
triple7
((triple3) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
((((triple4) -> (rule2 % int2))) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
triple8
Harry is round.
("Harry" "is" "round" "+")
triple9
Harry is white.
("Harry" "is" "white" "+")
triple10
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple8) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
((((triple8) -> (rule2 % int2))) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2