Anne is not big. Dave is rough. Fiona is white. Harry is cold. If something is white then it is young. Cold, white things are young. All young, white things are cold. All rough, white things are not cold. Cold things are not red. Rough things are big.
Anne is not big.
("Anne" "is" "big" "-")
Dave is rough.
("Dave" "is" "rough" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Harry is cold.
("Harry" "is" "cold" "+")
If something is white then it is young.
((("something" "is" "white" "+")) -> ("something" "is" "young" "+"))
Cold, white things are young.
((("something" "is" "cold" "+") ("something" "is" "white" "+")) -> ("something" "is" "young" "+"))
All young, white things are cold.
((("something" "is" "young" "+") ("something" "is" "white" "+")) -> ("something" "is" "cold" "+"))
All rough, white things are not cold.
((("something" "is" "rough" "+") ("something" "is" "white" "+")) -> ("something" "is" "cold" "-"))
Cold things are not red.
((("something" "is" "cold" "+")) -> ("something" "is" "red" "-"))
Rough things are big.
((("something" "is" "rough" "+")) -> ("something" "is" "big" "+"))
Dave is rough.
True
1
proof
[(triple2)]
("Dave" "is" "rough" "+")
triple2
Anne is big.
False
1
inv-proof
[(triple1)]
("Anne" "is" "big" "+")
triple1
Fiona is young.
True
2
proof
[(((triple3) -> rule1))]
("Fiona" "is" "young" "+")
((triple3) -> (rule1 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Harry is red.
False
2
inv-proof
[(((triple4) -> rule5))]
("Harry" "is" "red" "+")
((triple4) -> (rule5 % int1))
Harry is not red.
("Harry" "is" "red" "-")
int1
Fiona is cold.
True
4
proof
[(((((triple3) -> rule1) triple3) -> rule3))]
("Fiona" "is" "cold" "+")
((((triple3) -> (rule1 % int2)) triple3) -> (rule3 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is not cold.
False
4
inv-proof
[(((((triple3) -> rule1) triple3) -> rule3))]
("Fiona" "is" "cold" "-")
((((triple3) -> (rule1 % int2)) triple3) -> (rule3 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is not red.
True
5
proof
[(((((((triple3) -> rule1) triple3) -> rule3)) -> rule5))]
("Fiona" "is" "red" "-")
((((((triple3) -> (rule1 % int3)) triple3) -> (rule3 % int2))) -> (rule5 % int1))
Fiona is not red.
("Fiona" "is" "red" "-")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is red.
False
5
inv-proof
[(((((((triple3) -> rule1) triple3) -> rule3)) -> rule5))]
("Fiona" "is" "red" "+")
((((((triple3) -> (rule1 % int3)) triple3) -> (rule3 % int2))) -> (rule5 % int1))
Fiona is not red.
("Fiona" "is" "red" "-")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Dave is not cold.
Unknown
inv-rconc
[@1: Dave is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "cold" "-")
Harry is young.
Unknown
rconc
[@1: Harry is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "young" "+")
Dave is not young.
Unknown
inv-rconc
[@1: Dave is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "young" "-")
Anne is cold.
Unknown
rconc
[@1: Anne is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "cold" "+")
Anne is not red.
Unknown
inv-random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "-")
Fiona is rough.
Unknown
random
[@0: Fiona is rough.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "rough" "+")
Harry is not rough.
Unknown
inv-random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "-")
Dave is red.
Unknown
random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "+")
@0: Anne is not big.[(triple1)] Dave is rough.[(triple2)] Fiona is white.[(triple3)] Harry is cold.[(triple4)] @1: Dave is big.[(((triple2) -> rule6))] Fiona is young.[(((triple3) -> rule1))] Harry is not red.[(((triple4) -> rule5))] @2: Fiona is cold.[(((((triple3) -> rule1) triple3) -> rule3))] @3: Fiona is not red.[(((((((triple3) -> rule1) triple3) -> rule3)) -> rule5))]
Anne is not big.
("Anne" "is" "big" "-")
triple1
Dave is rough.
("Dave" "is" "rough" "+")
triple2
Fiona is white.
("Fiona" "is" "white" "+")
triple3
Harry is cold.
("Harry" "is" "cold" "+")
triple4
Dave is big.
("Dave" "is" "big" "+")
((triple2) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
((triple3) -> (rule1 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Harry is not red.
("Harry" "is" "red" "-")
((triple4) -> (rule5 % int1))
Harry is not red.
("Harry" "is" "red" "-")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
((((triple3) -> (rule1 % int2)) triple3) -> (rule3 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is not red.
("Fiona" "is" "red" "-")
((((((triple3) -> (rule1 % int3)) triple3) -> (rule3 % int2))) -> (rule5 % int1))
Fiona is not red.
("Fiona" "is" "red" "-")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3