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