Anne is nice. Charlie is big. Fiona is red. Harry is cold. If someone is big then they are smart. Rough people are big. Cold people are rough.
Anne is nice.
("Anne" "is" "nice" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Harry is cold.
("Harry" "is" "cold" "+")
If someone is big then they are smart.
((("someone" "is" "big" "+")) -> ("someone" "is" "smart" "+"))
Rough people are big.
((("someone" "is" "rough" "+")) -> ("someone" "is" "big" "+"))
Cold people are rough.
((("someone" "is" "cold" "+")) -> ("someone" "is" "rough" "+"))
Fiona is red.
True
1
proof
[(triple3)]
("Fiona" "is" "red" "+")
triple3
Anne is not nice.
False
1
inv-proof
[(triple1)]
("Anne" "is" "nice" "-")
triple1
Harry is rough.
True
2
proof
[(((triple4) -> rule3))]
("Harry" "is" "rough" "+")
((triple4) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is not rough.
False
2
inv-proof
[(((triple4) -> rule3))]
("Harry" "is" "rough" "-")
((triple4) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is big.
True
3
proof
[(((((triple4) -> rule3)) -> rule2))]
("Harry" "is" "big" "+")
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is not big.
False
3
inv-proof
[(((((triple4) -> rule3)) -> rule2))]
("Harry" "is" "big" "-")
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is smart.
True
4
proof
[(((((((triple4) -> rule3)) -> rule2)) -> rule1))]
("Harry" "is" "smart" "+")
((((((triple4) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is not smart.
False
4
inv-proof
[(((((((triple4) -> rule3)) -> rule2)) -> rule1))]
("Harry" "is" "smart" "-")
((((((triple4) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Fiona is not smart.
Unknown
inv-rconc
[@3: Fiona is smart.[CWA. Example of deepest failure = (rule1 <- rule2 <- rule3 <- FAIL)]]
("Fiona" "is" "smart" "-")
Fiona is rough.
Unknown
rconc
[@1: Fiona is rough.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "rough" "+")
Anne is not smart.
Unknown
inv-rconc
[@3: Anne is smart.[CWA. Example of deepest failure = (rule1 <- rule2 <- rule3 <- FAIL)]]
("Anne" "is" "smart" "-")
Charlie is rough.
Unknown
rconc
[@1: Charlie is rough.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "rough" "+")
Fiona is not quiet.
Unknown
inv-random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "-")
Charlie is cold.
Unknown
random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "+")
Harry is not red.
Unknown
inv-random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "-")
Charlie is quiet.
Unknown
random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "+")
@0: Anne is nice.[(triple1)] Charlie is big.[(triple2)] Fiona is red.[(triple3)] Harry is cold.[(triple4)] @1: Charlie is smart.[(((triple2) -> rule1))] Harry is rough.[(((triple4) -> rule3))] @2: Harry is big.[(((((triple4) -> rule3)) -> rule2))] @3: Harry is smart.[(((((((triple4) -> rule3)) -> rule2)) -> rule1))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Charlie is big.
("Charlie" "is" "big" "+")
triple2
Fiona is red.
("Fiona" "is" "red" "+")
triple3
Harry is cold.
("Harry" "is" "cold" "+")
triple4
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple2) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
((triple4) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
((((((triple4) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3