Anne is cold. Anne is young. Charlie is smart. Dave is big. Dave is green. Dave is round. Fiona is green. All cold things are big. If something is big and cold then it is green. Green things are smart.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is young.
("Anne" "is" "young" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is round.
("Dave" "is" "round" "+")
Fiona is green.
("Fiona" "is" "green" "+")
All cold things are big.
((("something" "is" "cold" "+")) -> ("something" "is" "big" "+"))
If something is big and cold then it is green.
((("something" "is" "big" "+") ("something" "is" "cold" "+")) -> ("something" "is" "green" "+"))
Green things are smart.
((("something" "is" "green" "+")) -> ("something" "is" "smart" "+"))
Anne is young.
True
1
proof
[(triple2)]
("Anne" "is" "young" "+")
triple2
Dave is not big.
False
1
inv-proof
[(triple4)]
("Dave" "is" "big" "-")
triple4
Anne is big.
True
2
proof
[(((triple1) -> rule1))]
("Anne" "is" "big" "+")
((triple1) -> (rule1 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Dave is not smart.
False
2
inv-proof
[(((triple5) -> rule3))]
("Dave" "is" "smart" "-")
((triple5) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Anne is green.
True
4
proof
[(((((triple1) -> rule1) triple1) -> rule2))]
("Anne" "is" "green" "+")
((((triple1) -> (rule1 % int2)) triple1) -> (rule2 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is not green.
False
4
inv-proof
[(((((triple1) -> rule1) triple1) -> rule2))]
("Anne" "is" "green" "-")
((((triple1) -> (rule1 % int2)) triple1) -> (rule2 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is smart.
True
5
proof
[(((((((triple1) -> rule1) triple1) -> rule2)) -> rule3))]
("Anne" "is" "smart" "+")
((((((triple1) -> (rule1 % int3)) triple1) -> (rule2 % int2))) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Anne is not smart.
False
5
inv-proof
[(((((((triple1) -> rule1) triple1) -> rule2)) -> rule3))]
("Anne" "is" "smart" "-")
((((((triple1) -> (rule1 % int3)) triple1) -> (rule2 % int2))) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Charlie is not green.
Unknown
inv-rconc
[@1: Charlie is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "green" "-")
Charlie is big.
Unknown
rconc
[@1: Charlie is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "big" "+")
Fiona is not big.
Unknown
inv-rconc
[@1: Fiona is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "big" "-")
Dave is young.
Unknown
random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "+")
Charlie is not young.
Unknown
inv-random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "-")
Fiona is young.
Unknown
random
[@0: Fiona is young.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "young" "+")
Charlie is not round.
Unknown
inv-random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
@0: Anne is cold.[(triple1)] Anne is young.[(triple2)] Charlie is smart.[(triple3)] Dave is big.[(triple4)] Dave is green.[(triple5)] Dave is round.[(triple6)] Fiona is green.[(triple7)] @1: Anne is big.[(((triple1) -> rule1))] Dave is smart.[(((triple5) -> rule3))] Fiona is smart.[(((triple7) -> rule3))] @2: Anne is green.[(((((triple1) -> rule1) triple1) -> rule2))] @3: Anne is smart.[(((((((triple1) -> rule1) triple1) -> rule2)) -> rule3))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is young.
("Anne" "is" "young" "+")
triple2
Charlie is smart.
("Charlie" "is" "smart" "+")
triple3
Dave is big.
("Dave" "is" "big" "+")
triple4
Dave is green.
("Dave" "is" "green" "+")
triple5
Dave is round.
("Dave" "is" "round" "+")
triple6
Fiona is green.
("Fiona" "is" "green" "+")
triple7
Anne is big.
("Anne" "is" "big" "+")
((triple1) -> (rule1 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
((triple5) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
((triple7) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
((((triple1) -> (rule1 % int2)) triple1) -> (rule2 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
((((((triple1) -> (rule1 % int3)) triple1) -> (rule2 % int2))) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3