Charlie is young. Fiona is rough. Harry is red. Red things are smart. If Fiona is smart then Fiona is young. If something is smart then it is red. All rough things are red. All quiet things are young. If something is smart then it is rough. If Fiona is red and Fiona is rough then Fiona is cold. Cold, quiet things are big.
Charlie is young.
("Charlie" "is" "young" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Harry is red.
("Harry" "is" "red" "+")
Red things are smart.
((("something" "is" "red" "+")) -> ("something" "is" "smart" "+"))
If Fiona is smart then Fiona is young.
((("Fiona" "is" "smart" "+")) -> ("Fiona" "is" "young" "+"))
If something is smart then it is red.
((("something" "is" "smart" "+")) -> ("something" "is" "red" "+"))
All rough things are red.
((("something" "is" "rough" "+")) -> ("something" "is" "red" "+"))
All quiet things are young.
((("something" "is" "quiet" "+")) -> ("something" "is" "young" "+"))
If something is smart then it is rough.
((("something" "is" "smart" "+")) -> ("something" "is" "rough" "+"))
If Fiona is red and Fiona is rough then Fiona is cold.
((("Fiona" "is" "red" "+") ("Fiona" "is" "rough" "+")) -> ("Fiona" "is" "cold" "+"))
Cold, quiet things are big.
((("something" "is" "cold" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "big" "+"))
Fiona is rough.
True
1
proof
[(triple2)]
("Fiona" "is" "rough" "+")
triple2
Charlie is not young.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "young" "-")
triple1
Fiona is red.
True
2
proof
[(((triple2) -> rule4))]
("Fiona" "is" "red" "+")
((triple2) -> (rule4 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is not red.
False
2
inv-proof
[(((triple2) -> rule4))]
("Fiona" "is" "red" "-")
((triple2) -> (rule4 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Harry is rough.
True
3
proof
[(((((triple3) -> rule1)) -> rule6))]
("Harry" "is" "rough" "+")
((((triple3) -> (rule1 % int2))) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is not rough.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule6))]
("Harry" "is" "rough" "-")
((((triple3) -> (rule1 % int2))) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Fiona is young.
True
4
proof
[(((((((triple2) -> rule4)) -> rule1)) -> rule2))]
("Fiona" "is" "young" "+")
((((((triple2) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
Fiona is not young.
False
4
inv-proof
[(((((((triple2) -> rule4)) -> rule1)) -> rule2))]
("Fiona" "is" "young" "-")
((((((triple2) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
Fiona is not big.
Unknown
inv-rconc
[@1: Fiona is big.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Fiona" "is" "big" "-")
Charlie is red.
Unknown
rconc
[@4: Charlie is red.[CWA. Example of deepest failure = (rule3 <- rule1 <- rule4 <- rule6 <- FAIL)]]
("Charlie" "is" "red" "+")
Charlie is not smart.
Unknown
inv-rconc
[@3: Charlie is smart.[CWA. Example of deepest failure = (rule1 <- rule4 <- rule6 <- FAIL)]]
("Charlie" "is" "smart" "-")
Charlie is big.
Unknown
rconc
[@1: Charlie is big.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Charlie" "is" "big" "+")
Charlie is not cold.
Unknown
inv-random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "-")
Harry is cold.
Unknown
random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "+")
Harry is not quiet.
Unknown
inv-random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "-")
Charlie is quiet.
Unknown
random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "+")
@0: Charlie is young.[(triple1)] Fiona is rough.[(triple2)] Harry is red.[(triple3)] @1: Fiona is red.[(((triple2) -> rule4))] Harry is smart.[(((triple3) -> rule1))] @2: Fiona is cold.[(((((triple2) -> rule4) triple2) -> rule7))] Fiona is smart.[(((((triple2) -> rule4)) -> rule1))] Harry is rough.[(((((triple3) -> rule1)) -> rule6))] @3: Fiona is young.[(((((((triple2) -> rule4)) -> rule1)) -> rule2))]
Charlie is young.
("Charlie" "is" "young" "+")
triple1
Fiona is rough.
("Fiona" "is" "rough" "+")
triple2
Harry is red.
("Harry" "is" "red" "+")
triple3
Fiona is red.
("Fiona" "is" "red" "+")
((triple2) -> (rule4 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
((triple3) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
((((triple2) -> (rule4 % int2)) triple2) -> (rule7 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
((((triple2) -> (rule4 % int2))) -> (rule1 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
((((triple3) -> (rule1 % int2))) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
((((((triple2) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3