Charlie is rough. Fiona is round. Harry is not rough. Rough people are big. Blue people are big. Nice people are not big. If Charlie is big and Charlie is round then Charlie is blue. All blue people are not nice. Rough people are round.
Charlie is rough.
("Charlie" "is" "rough" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Harry is not rough.
("Harry" "is" "rough" "-")
Rough people are big.
((("someone" "is" "rough" "+")) -> ("someone" "is" "big" "+"))
Blue people are big.
((("someone" "is" "blue" "+")) -> ("someone" "is" "big" "+"))
Nice people are not big.
((("someone" "is" "nice" "+")) -> ("someone" "is" "big" "-"))
If Charlie is big and Charlie is round then Charlie is blue.
((("Charlie" "is" "big" "+") ("Charlie" "is" "round" "+")) -> ("Charlie" "is" "blue" "+"))
All blue people are not nice.
((("someone" "is" "blue" "+")) -> ("someone" "is" "nice" "-"))
Rough people are round.
((("someone" "is" "rough" "+")) -> ("someone" "is" "round" "+"))
Harry is not rough.
True
1
proof
[(triple3)]
("Harry" "is" "rough" "-")
triple3
Charlie is not rough.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "rough" "-")
triple1
Charlie is round.
True
2
proof
[(((triple1) -> rule6))]
("Charlie" "is" "round" "+")
((triple1) -> (rule6 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is not round.
False
2
inv-proof
[(((triple1) -> rule6))]
("Charlie" "is" "round" "-")
((triple1) -> (rule6 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is blue.
True
5
proof
[(((((triple1) -> rule1) ((triple1) -> rule6)) -> rule4))]
("Charlie" "is" "blue" "+")
((((triple1) -> (rule1 % int3)) ((triple1) -> (rule6 % int2))) -> (rule4 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is not blue.
False
5
inv-proof
[(((((triple1) -> rule1) ((triple1) -> rule6)) -> rule4))]
("Charlie" "is" "blue" "-")
((((triple1) -> (rule1 % int3)) ((triple1) -> (rule6 % int2))) -> (rule4 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is not nice.
True
6
proof
[(((((((triple1) -> rule1) ((triple1) -> rule6)) -> rule4)) -> rule5))]
("Charlie" "is" "nice" "-")
((((((triple1) -> (rule1 % int4)) ((triple1) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Charlie is not nice.
("Charlie" "is" "nice" "-")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is big.
("Charlie" "is" "big" "+")
int4
Charlie is nice.
False
6
inv-proof
[(((((((triple1) -> rule1) ((triple1) -> rule6)) -> rule4)) -> rule5))]
("Charlie" "is" "nice" "+")
((((((triple1) -> (rule1 % int4)) ((triple1) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Charlie is not nice.
("Charlie" "is" "nice" "-")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is big.
("Charlie" "is" "big" "+")
int4
Fiona is not big.
Unknown
inv-rconc
[@1: Fiona is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "big" "-")
Harry is round.
Unknown
rconc
[@1: Harry is round.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "round" "+")
Harry is not big.
Unknown
inv-rconc
[@1: Harry is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "big" "-")
Fiona is blue.
Unknown
random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "+")
Charlie is not furry.
Unknown
inv-random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "-")
Harry is smart.
Unknown
random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "+")
Harry is not furry.
Unknown
inv-random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "-")
Fiona is rough.
Unknown
random
[@0: Fiona is rough.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "rough" "+")
@0: Charlie is rough.[(triple1)] Fiona is round.[(triple2)] Harry is not rough.[(triple3)] @1: Charlie is big.[(((triple1) -> rule1))] Charlie is round.[(((triple1) -> rule6))] @2: Charlie is blue.[(((((triple1) -> rule1) ((triple1) -> rule6)) -> rule4))] @3: Charlie is not nice.[(((((((triple1) -> rule1) ((triple1) -> rule6)) -> rule4)) -> rule5))]
Charlie is rough.
("Charlie" "is" "rough" "+")
triple1
Fiona is round.
("Fiona" "is" "round" "+")
triple2
Harry is not rough.
("Harry" "is" "rough" "-")
triple3
Charlie is big.
("Charlie" "is" "big" "+")
((triple1) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
((triple1) -> (rule6 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
((((triple1) -> (rule1 % int3)) ((triple1) -> (rule6 % int2))) -> (rule4 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is not nice.
("Charlie" "is" "nice" "-")
((((((triple1) -> (rule1 % int4)) ((triple1) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Charlie is not nice.
("Charlie" "is" "nice" "-")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is big.
("Charlie" "is" "big" "+")
int4