Bob is rough. Charlie is cold. Fiona is big. Harry is furry. All kind people are furry. Furry, cold people are nice. All big people are cold. If Fiona is smart then Fiona is rough. All cold, kind people are rough. If someone is cold then they are smart.
Bob is rough.
("Bob" "is" "rough" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Harry is furry.
("Harry" "is" "furry" "+")
All kind people are furry.
((("someone" "is" "kind" "+")) -> ("someone" "is" "furry" "+"))
Furry, cold people are nice.
((("someone" "is" "furry" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "nice" "+"))
All big people are cold.
((("someone" "is" "big" "+")) -> ("someone" "is" "cold" "+"))
If Fiona is smart then Fiona is rough.
((("Fiona" "is" "smart" "+")) -> ("Fiona" "is" "rough" "+"))
All cold, kind people are rough.
((("someone" "is" "cold" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "rough" "+"))
If someone is cold then they are smart.
((("someone" "is" "cold" "+")) -> ("someone" "is" "smart" "+"))
Bob is rough.
True
1
proof
[(triple1)]
("Bob" "is" "rough" "+")
triple1
Bob is not rough.
False
1
inv-proof
[(triple1)]
("Bob" "is" "rough" "-")
triple1
Charlie is smart.
True
2
proof
[(((triple2) -> rule6))]
("Charlie" "is" "smart" "+")
((triple2) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Fiona is not cold.
False
2
inv-proof
[(((triple3) -> rule3))]
("Fiona" "is" "cold" "-")
((triple3) -> (rule3 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is smart.
True
3
proof
[(((((triple3) -> rule3)) -> rule6))]
("Fiona" "is" "smart" "+")
((((triple3) -> (rule3 % int2))) -> (rule6 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is not smart.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule6))]
("Fiona" "is" "smart" "-")
((((triple3) -> (rule3 % int2))) -> (rule6 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Harry is not rough.
Unknown
inv-rconc
[@1: Harry is rough.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Harry" "is" "rough" "-")
Fiona is furry.
Unknown
rconc
[@1: Fiona is furry.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "furry" "+")
Fiona is not nice.
Unknown
inv-rconc
[@2: Fiona is nice.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Fiona" "is" "nice" "-")
Charlie is big.
Unknown
random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "+")
Charlie is not kind.
Unknown
inv-random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "-")
Fiona is kind.
Unknown
random
[@0: Fiona is kind.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "kind" "+")
@0: Bob is rough.[(triple1)] Charlie is cold.[(triple2)] Fiona is big.[(triple3)] Harry is furry.[(triple4)] @1: Charlie is smart.[(((triple2) -> rule6))] Fiona is cold.[(((triple3) -> rule3))] @2: Fiona is smart.[(((((triple3) -> rule3)) -> rule6))] @3: Fiona is rough.[(((((((triple3) -> rule3)) -> rule6)) -> rule4))]
Bob is rough.
("Bob" "is" "rough" "+")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
Fiona is big.
("Fiona" "is" "big" "+")
triple3
Harry is furry.
("Harry" "is" "furry" "+")
triple4
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple2) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
((triple3) -> (rule3 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
((((triple3) -> (rule3 % int2))) -> (rule6 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
((((((triple3) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3