Bob is round. Charlie is green. Harry is quiet. All young things are nice. If something is green then it is red. All green, red things are young.
Bob is round.
("Bob" "is" "round" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
All young things are nice.
((("something" "is" "young" "+")) -> ("something" "is" "nice" "+"))
If something is green then it is red.
((("something" "is" "green" "+")) -> ("something" "is" "red" "+"))
All green, red things are young.
((("something" "is" "green" "+") ("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
Harry is quiet.
True
1
proof
[(triple3)]
("Harry" "is" "quiet" "+")
triple3
Charlie is not green.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "green" "-")
triple2
Charlie is red.
True
2
proof
[(((triple2) -> rule2))]
("Charlie" "is" "red" "+")
((triple2) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is not red.
False
2
inv-proof
[(((triple2) -> rule2))]
("Charlie" "is" "red" "-")
((triple2) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is young.
True
4
proof
[(((triple2 ((triple2) -> rule2)) -> rule3))]
("Charlie" "is" "young" "+")
((triple2 ((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is not young.
False
4
inv-proof
[(((triple2 ((triple2) -> rule2)) -> rule3))]
("Charlie" "is" "young" "-")
((triple2 ((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is nice.
True
5
proof
[(((((triple2 ((triple2) -> rule2)) -> rule3)) -> rule1))]
("Charlie" "is" "nice" "+")
((((triple2 ((triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Charlie is not nice.
False
5
inv-proof
[(((((triple2 ((triple2) -> rule2)) -> rule3)) -> rule1))]
("Charlie" "is" "nice" "-")
((((triple2 ((triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Bob is not young.
Unknown
inv-rconc
[@1: Bob is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "young" "-")
Harry is nice.
Unknown
rconc
[@2: Harry is nice.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Harry" "is" "nice" "+")
Bob is not red.
Unknown
inv-rconc
[@1: Bob is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "red" "-")
Bob is nice.
Unknown
rconc
[@2: Bob is nice.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Bob" "is" "nice" "+")
Charlie is not quiet.
Unknown
inv-random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "-")
Charlie is furry.
Unknown
random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "+")
Bob is not furry.
Unknown
inv-random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "-")
Harry is round.
Unknown
random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "+")
@0: Bob is round.[(triple1)] Charlie is green.[(triple2)] Harry is quiet.[(triple3)] @1: Charlie is red.[(((triple2) -> rule2))] @2: Charlie is young.[(((triple2 ((triple2) -> rule2)) -> rule3))] @3: Charlie is nice.[(((((triple2 ((triple2) -> rule2)) -> rule3)) -> rule1))]
Bob is round.
("Bob" "is" "round" "+")
triple1
Charlie is green.
("Charlie" "is" "green" "+")
triple2
Harry is quiet.
("Harry" "is" "quiet" "+")
triple3
Charlie is red.
("Charlie" "is" "red" "+")
((triple2) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
((triple2 ((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
((((triple2 ((triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3