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