Anne is green. Anne is young. Bob is blue. Bob is smart. Bob is young. Erin is blue. Erin is furry. Erin is green. Erin is young. Gary is blue. All round people are smart. If someone is young then they are round. Smart people are cold.
Anne is green.
("Anne" "is" "green" "+")
Anne is young.
("Anne" "is" "young" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is young.
("Bob" "is" "young" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is young.
("Erin" "is" "young" "+")
Gary is blue.
("Gary" "is" "blue" "+")
All round people are smart.
((("someone" "is" "round" "+")) -> ("someone" "is" "smart" "+"))
If someone is young then they are round.
((("someone" "is" "young" "+")) -> ("someone" "is" "round" "+"))
Smart people are cold.
((("someone" "is" "smart" "+")) -> ("someone" "is" "cold" "+"))
Bob is blue.
True
1
proof
[(triple3)]
("Bob" "is" "blue" "+")
triple3
Bob is not smart.
False
1
inv-proof
[(triple4 OR ((((triple5) -> rule2)) -> rule1))]
("Bob" "is" "smart" "-")
triple4
((((triple5) -> (rule2 % int2))) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Anne is round.
True
2
proof
[(((triple2) -> rule2))]
("Anne" "is" "round" "+")
((triple2) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Bob is not round.
False
2
inv-proof
[(((triple5) -> rule2))]
("Bob" "is" "round" "-")
((triple5) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Erin is smart.
True
3
proof
[(((((triple9) -> rule2)) -> rule1))]
("Erin" "is" "smart" "+")
((((triple9) -> (rule2 % int2))) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is not smart.
False
3
inv-proof
[(((((triple9) -> rule2)) -> rule1))]
("Erin" "is" "smart" "-")
((((triple9) -> (rule2 % int2))) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Anne is cold.
True
4
proof
[(((((((triple2) -> rule2)) -> rule1)) -> rule3))]
("Anne" "is" "cold" "+")
((((((triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Erin is not cold.
False
4
inv-proof
[(((((((triple9) -> rule2)) -> rule1)) -> rule3))]
("Erin" "is" "cold" "-")
((((((triple9) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Gary is not round.
Unknown
inv-rconc
[@1: Gary is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "round" "-")
Gary is smart.
Unknown
rconc
[@2: Gary is smart.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Gary" "is" "smart" "+")
Gary is not cold.
Unknown
inv-rconc
[@3: Gary is cold.[CWA. Example of deepest failure = (rule3 <- rule1 <- rule2 <- FAIL)]]
("Gary" "is" "cold" "-")
Gary is green.
Unknown
random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "+")
Gary is not young.
Unknown
inv-random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "-")
Anne is furry.
Unknown
random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "+")
Anne is not blue.
Unknown
inv-random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "-")
Bob is green.
Unknown
random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "+")
@0: Anne is green.[(triple1)] Anne is young.[(triple2)] Bob is blue.[(triple3)] Bob is smart.[(triple4 OR ((((triple5) -> rule2)) -> rule1))] Bob is young.[(triple5)] Erin is blue.[(triple6)] Erin is furry.[(triple7)] Erin is green.[(triple8)] Erin is young.[(triple9)] Gary is blue.[(triple10)] @1: Anne is round.[(((triple2) -> rule2))] Bob is cold.[(((triple4) -> rule3) OR ((((((triple5) -> rule2)) -> rule1)) -> rule3))] Bob is round.[(((triple5) -> rule2))] Erin is round.[(((triple9) -> rule2))] @2: Anne is smart.[(((((triple2) -> rule2)) -> rule1))] Erin is smart.[(((((triple9) -> rule2)) -> rule1))] @3: Anne is cold.[(((((((triple2) -> rule2)) -> rule1)) -> rule3))] Erin is cold.[(((((((triple9) -> rule2)) -> rule1)) -> rule3))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Anne is young.
("Anne" "is" "young" "+")
triple2
Bob is blue.
("Bob" "is" "blue" "+")
triple3
Bob is smart.
("Bob" "is" "smart" "+")
triple4
((((triple5) -> (rule2 % int2))) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
triple5
Erin is blue.
("Erin" "is" "blue" "+")
triple6
Erin is furry.
("Erin" "is" "furry" "+")
triple7
Erin is green.
("Erin" "is" "green" "+")
triple8
Erin is young.
("Erin" "is" "young" "+")
triple9
Gary is blue.
("Gary" "is" "blue" "+")
triple10
Anne is round.
("Anne" "is" "round" "+")
((triple2) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
((triple4) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
((((((triple5) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is round.
("Bob" "is" "round" "+")
((triple5) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
((triple9) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
((((triple9) -> (rule2 % int2))) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
((((((triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Erin is cold.
("Erin" "is" "cold" "+")
((((((triple9) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3