Charlie is big. Fiona is blue. Harry is red. Rough things are big. If something is blue then it is rough. If Harry is big and Harry is red then Harry is rough.
Charlie is big.
("Charlie" "is" "big" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Harry is red.
("Harry" "is" "red" "+")
Rough things are big.
((("something" "is" "rough" "+")) -> ("something" "is" "big" "+"))
If something is blue then it is rough.
((("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
If Harry is big and Harry is red then Harry is rough.
((("Harry" "is" "big" "+") ("Harry" "is" "red" "+")) -> ("Harry" "is" "rough" "+"))
Fiona is blue.
True
1
proof
[(triple2)]
("Fiona" "is" "blue" "+")
triple2
Harry is not red.
False
1
inv-proof
[(triple3)]
("Harry" "is" "red" "-")
triple3
Fiona is rough.
True
2
proof
[(((triple2) -> rule2))]
("Fiona" "is" "rough" "+")
((triple2) -> (rule2 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is not rough.
False
2
inv-proof
[(((triple2) -> rule2))]
("Fiona" "is" "rough" "-")
((triple2) -> (rule2 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is big.
True
3
proof
[(((((triple2) -> rule2)) -> rule1))]
("Fiona" "is" "big" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is not big.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule1))]
("Fiona" "is" "big" "-")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Harry is not rough.
Unknown
inv-rconc
[@3: Harry is rough.[CWA. Example of deepest failure = (rule3 <- rule1 <- rule2 <- FAIL)]]
("Harry" "is" "rough" "-")
Charlie is rough.
Unknown
rconc
[@1: Charlie is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "rough" "+")
Harry is not big.
Unknown
inv-rconc
[@2: Harry is big.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Harry" "is" "big" "-")
Charlie is young.
Unknown
random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "+")
Charlie is not red.
Unknown
inv-random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "-")
Fiona is red.
Unknown
random
[@0: Fiona is red.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "red" "+")
@0: Charlie is big.[(triple1)] Fiona is blue.[(triple2)] Harry is red.[(triple3)] @1: Fiona is rough.[(((triple2) -> rule2))] @2: Fiona is big.[(((((triple2) -> rule2)) -> rule1))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Fiona is blue.
("Fiona" "is" "blue" "+")
triple2
Harry is red.
("Harry" "is" "red" "+")
triple3
Fiona is rough.
("Fiona" "is" "rough" "+")
((triple2) -> (rule2 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2