Bob is red. Erin is quiet. Gary is blue. Harry is young. If Bob is blue and Bob is red then Bob is round. All round people are green. Round, quiet people are young. All green people are young. Green people are round. Green people are furry. If Gary is furry then Gary is quiet. If someone is red then they are blue.
Bob is red.
("Bob" "is" "red" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Harry is young.
("Harry" "is" "young" "+")
If Bob is blue and Bob is red then Bob is round.
((("Bob" "is" "blue" "+") ("Bob" "is" "red" "+")) -> ("Bob" "is" "round" "+"))
All round people are green.
((("someone" "is" "round" "+")) -> ("someone" "is" "green" "+"))
Round, quiet people are young.
((("someone" "is" "round" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "young" "+"))
All green people are young.
((("someone" "is" "green" "+")) -> ("someone" "is" "young" "+"))
Green people are round.
((("someone" "is" "green" "+")) -> ("someone" "is" "round" "+"))
Green people are furry.
((("someone" "is" "green" "+")) -> ("someone" "is" "furry" "+"))
If Gary is furry then Gary is quiet.
((("Gary" "is" "furry" "+")) -> ("Gary" "is" "quiet" "+"))
If someone is red then they are blue.
((("someone" "is" "red" "+")) -> ("someone" "is" "blue" "+"))
Erin is quiet.
True
1
proof
[(triple2)]
("Erin" "is" "quiet" "+")
triple2
Bob is not red.
False
1
inv-proof
[(triple1)]
("Bob" "is" "red" "-")
triple1
Bob is blue.
True
2
proof
[(((triple1) -> rule8))]
("Bob" "is" "blue" "+")
((triple1) -> (rule8 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is not blue.
False
2
inv-proof
[(((triple1) -> rule8))]
("Bob" "is" "blue" "-")
((triple1) -> (rule8 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is round.
True
4
proof
[(((((triple1) -> rule8) triple1) -> rule1))]
("Bob" "is" "round" "+")
((((triple1) -> (rule8 % int2)) triple1) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is not round.
False
4
inv-proof
[(((((triple1) -> rule8) triple1) -> rule1))]
("Bob" "is" "round" "-")
((((triple1) -> (rule8 % int2)) triple1) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is green.
True
5
proof
[(((((((triple1) -> rule8) triple1) -> rule1)) -> rule2))]
("Bob" "is" "green" "+")
((((((triple1) -> (rule8 % int3)) triple1) -> (rule1 % int2))) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is not green.
False
5
inv-proof
[(((((((triple1) -> rule8) triple1) -> rule1)) -> rule2))]
("Bob" "is" "green" "-")
((((((triple1) -> (rule8 % int3)) triple1) -> (rule1 % int2))) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Erin is not green.
Unknown
inv-rconc
[@2: Erin is green.[CWA. Example of deepest failure = (rule2 <- rule5 <- FAIL)]]
("Erin" "is" "green" "-")
Harry is green.
Unknown
rconc
[@2: Harry is green.[CWA. Example of deepest failure = (rule2 <- rule5 <- FAIL)]]
("Harry" "is" "green" "+")
Harry is not round.
Unknown
inv-rconc
[@2: Harry is round.[CWA. Example of deepest failure = (rule5 <- rule2 <- FAIL)]]
("Harry" "is" "round" "-")
Harry is blue.
Unknown
rconc
[@1: Harry is blue.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Harry" "is" "blue" "+")
Erin is not red.
Unknown
inv-random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "-")
Gary is red.
Unknown
random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "+")
Bob is not quiet.
Unknown
inv-random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "-")
Harry is quiet.
Unknown
random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "+")
@0: Bob is red.[(triple1)] Erin is quiet.[(triple2)] Gary is blue.[(triple3)] Harry is young.[(triple4)] @1: Bob is blue.[(((triple1) -> rule8))] @2: Bob is round.[(((((triple1) -> rule8) triple1) -> rule1))] @3: Bob is green.[(((((((triple1) -> rule8) triple1) -> rule1)) -> rule2))] @4: Bob is furry.[(((((((((triple1) -> rule8) triple1) -> rule1)) -> rule2)) -> rule6))] Bob is young.[(((((((((triple1) -> rule8) triple1) -> rule1)) -> rule2)) -> rule4))]
Bob is red.
("Bob" "is" "red" "+")
triple1
Erin is quiet.
("Erin" "is" "quiet" "+")
triple2
Gary is blue.
("Gary" "is" "blue" "+")
triple3
Harry is young.
("Harry" "is" "young" "+")
triple4
Bob is blue.
("Bob" "is" "blue" "+")
((triple1) -> (rule8 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
((((triple1) -> (rule8 % int2)) triple1) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
((((((triple1) -> (rule8 % int3)) triple1) -> (rule1 % int2))) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is furry.
("Bob" "is" "furry" "+")
((((((((triple1) -> (rule8 % int4)) triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is blue.
("Bob" "is" "blue" "+")
int4
Bob is young.
("Bob" "is" "young" "+")
((((((((triple1) -> (rule8 % int4)) triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is blue.
("Bob" "is" "blue" "+")
int4